Z3_Proof.subst_types (line 215 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.lin_proof (line 290 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.lin_proof (line 290 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.lin_proof (line 290 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.lin_proof (line 290 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.lin_proof (line 290 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.lin_proof (line 290 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.lin_proof (line 290 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.lin_proof (line 290 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.lin_proof (line 290 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.lin_proof (line 290 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.lin_proof (line 290 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.lin_proof (line 290 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.lin_proof (line 290 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.lin_proof (line 290 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.lin_proof (line 290 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.lin_proof (line 290 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.lin_proof (line 290 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.linearize (line 305 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Proof.parse (line 311 of "~~/src/HOL/Tools/SMT/z3_proof.ML")
  Z3_Replay.replay (line 238 of "~~/src/HOL/Tools/SMT/z3_replay.ML")
  SMT_Solver.replay (line 201 of "~~/src/HOL/Tools/SMT/smt_solver.ML")
  SMT_Solver.apply_solver_and_replay (line 240 of "~~/src/HOL/Tools/SMT/smt_solver.ML")
  SMT_Solver.safe_solve (line 282 of "~~/src/HOL/Tools/SMT/smt_solver.ML")
  SMT_Solver.tac(3)(6) (line 298 of "~~/src/HOL/Tools/SMT/smt_solver.ML")
  Library.oo (line 239 of "library.ML")
  Subgoal.GEN_FOCUS (line 150 of "Isar/subgoal.ML")
  Seq.maps(2)(1) (line 173 of "General/seq.ML")
  Seq.pull (line 72 of "General/seq.ML")
  Seq.append(2)copy(1)(1) (line 125 of "General/seq.ML")
  Seq.pull (line 72 of "General/seq.ML")
  Seq.maps(2)(1) (line 173 of "General/seq.ML")
  Seq.pull (line 72 of "General/seq.ML")
  Seq.map(2)(1) (line 167 of "General/seq.ML")
  Seq.pull (line 72 of "General/seq.ML")
  Seq.append(2)copy(1)(1) (line 125 of "General/seq.ML")
  Seq.pull (line 72 of "General/seq.ML")
  Seq.maps_results(2)(1) (line 215 of "General/seq.ML")
  Seq.pull (line 72 of "General/seq.ML")
  Seq.maps_results(2)(1) (line 215 of "General/seq.ML")
  Seq.pull (line 72 of "General/seq.ML")
  Seq.maps_results(2)(1) (line 215 of "General/seq.ML")
  Seq.pull (line 72 of "General/seq.ML")
  Seq.append(2)copy(1)(1) (line 125 of "General/seq.ML")
  Seq.pull (line 72 of "General/seq.ML")
  Seq.first_result(2)result (line 227 of "General/seq.ML")
  Seq.first_result (line 225 of "General/seq.ML")
  Proof_Node.applys (line 44 of "Isar/proof_node.ML")
  Toplevel.proofs'(1)(1)(1) (line 503 of "Isar/toplevel.ML")
  Toplevel.apply_tr(3)(1) (line 265 of "Isar/toplevel.ML") 
exception Option raised (line 82 of "General/basics.ML")