src/Pure/Isar/toplevel.ML
changeset 47881 45a3a1c320d8
parent 47425 45e570742e73
child 48633 7cd32f9d4293
equal deleted inserted replaced
47880:7e202f71a249 47881:45a3a1c320d8
   186   (case node_of state of
   186   (case node_of state of
   187     Proof (prf, _) => Proof_Node.position prf
   187     Proof (prf, _) => Proof_Node.position prf
   188   | _ => raise UNDEF);
   188   | _ => raise UNDEF);
   189 
   189 
   190 fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
   190 fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
   191   | end_theory pos (State (NONE, _)) = error ("Missing theory" ^ Position.str_of pos)
   191   | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.str_of pos)
   192   | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.str_of pos);
   192   | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.str_of pos);
   193 
   193 
   194 
   194 
   195 (* print state *)
   195 (* print state *)
   196 
   196