src/Pure/Isar/toplevel.ML
changeset 12009 cbd35a736954
parent 11894 39a3ece43772
child 12049 58a2e6750d23
equal deleted inserted replaced
12008:078637472921 12009:cbd35a736954
   153 val theory_of = node_case I Proof.theory_of;
   153 val theory_of = node_case I Proof.theory_of;
   154 val context_of = node_case ProofContext.init Proof.context_of;
   154 val context_of = node_case ProofContext.init Proof.context_of;
   155 val sign_of = Theory.sign_of o theory_of;
   155 val sign_of = Theory.sign_of o theory_of;
   156 val proof_of = node_case (fn _ => raise UNDEF) I;
   156 val proof_of = node_case (fn _ => raise UNDEF) I;
   157 
   157 
   158 val enter_forward_proof = node_case Proof.init_state Proof.enter_forward;
   158 val enter_forward_proof = node_case (fn thy => Proof.init_state thy None) Proof.enter_forward;
   159 
   159 
   160 
   160 
   161 (** toplevel transitions **)
   161 (** toplevel transitions **)
   162 
   162 
   163 exception TERMINATE;
   163 exception TERMINATE;