src/Pure/Isar/toplevel.ML
changeset 68876 cefaac3d24ff
parent 68875 7f0151c951e3
child 68877 33d78e5e0a00
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sun Sep 02 13:53:55 2018 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Sep 02 14:14:43 2018 +0200
     1.3 @@ -65,7 +65,7 @@
     1.4      (local_theory -> Proof.state) -> transition -> transition
     1.5    val theory_to_proof: (theory -> Proof.state) -> transition -> transition
     1.6    val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
     1.7 -  val forget_proof: bool -> transition -> transition
     1.8 +  val forget_proof: transition -> transition
     1.9    val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
    1.10    val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
    1.11    val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
    1.12 @@ -517,10 +517,10 @@
    1.13  
    1.14  end;
    1.15  
    1.16 -fun forget_proof strict = transaction (fn _ =>
    1.17 +val forget_proof = transaction (fn _ =>
    1.18    (fn Proof (prf, (_, orig_gthy)) =>
    1.19 -        if strict andalso Proof.is_notepad (Proof_Node.current prf)
    1.20 -        then raise UNDEF else Theory (orig_gthy, NONE)
    1.21 +        if Proof.is_notepad (Proof_Node.current prf) then raise UNDEF
    1.22 +        else Theory (orig_gthy, NONE)
    1.23      | Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
    1.24      | _ => raise UNDEF));
    1.25  
    1.26 @@ -634,7 +634,7 @@
    1.27  
    1.28  in
    1.29  
    1.30 -val reset_theory = reset_state is_theory (forget_proof false);
    1.31 +val reset_theory = reset_state is_theory forget_proof;
    1.32  
    1.33  val reset_proof =
    1.34    reset_state is_proof