src/Pure/Isar/toplevel.ML

     (bool -> local_theory -> Proof.state) -> transition -> transition
   val local_theory_to_proof: (bool * Position.T) option -> (xstring * Position.T) option ->
     (local_theory -> Proof.state) -> transition -> transition
   val theory_to_proof: (theory -> Proof.state) -> transition -> transition
   val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
-  val forget_proof: bool -> transition -> transition
+  val forget_proof: transition -> transition
   val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
   val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
   val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
   val proof: (Proof.state -> Proof.state) -> transition -> transition
   val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition

         Context.Theory thy => f (Sign.new_group thy)
       | _ => raise UNDEF)));
 
 end;
 
-fun forget_proof strict = transaction (fn _ =>
+val forget_proof = transaction (fn _ =>
   (fn Proof (prf, (_, orig_gthy)) =>
-        if strict andalso Proof.is_notepad (Proof_Node.current prf)
-        then raise UNDEF else Theory (orig_gthy, NONE)
+        if Proof.is_notepad (Proof_Node.current prf) then raise UNDEF
+        else Theory (orig_gthy, NONE)
     | Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
     | _ => raise UNDEF));
 
 fun proofs' f = transaction (fn int =>
   (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x)

   if check st then NONE
   else #2 (command_errors false (trans empty) st);
 
 in
 
-val reset_theory = reset_state is_theory (forget_proof false);
+val reset_theory = reset_state is_theory forget_proof;
 
 val reset_proof =
   reset_state is_proof
     (transaction (fn _ =>
       (fn Theory (gthy, _) => Skipped_Proof (0, (gthy, gthy))