export init_state;
authorwenzelm
Thu Jul 15 17:53:28 1999 +0200 (1999-07-15)
changeset 70117e8e9a26ba2c
parent 7010 63120b6dca50
child 7012 ae9dac5af9d1
export init_state;
end_proof: reset goal_facts;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Thu Jul 15 10:34:37 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Jul 15 17:53:28 1999 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    type state
     1.5    exception STATE of string * state
     1.6    val check_result: string -> state -> 'a Seq.seq -> 'a Seq.seq
     1.7 +  val init_state: theory -> state
     1.8    val context_of: state -> context
     1.9    val theory_of: state -> theory
    1.10    val sign_of: state -> Sign.sg
    1.11 @@ -643,7 +644,8 @@
    1.12    |> assert_forward
    1.13    |> close_block
    1.14    |> assert_bottom bot
    1.15 -  |> assert_current_goal true;
    1.16 +  |> assert_current_goal true
    1.17 +  |> goal_facts (K []);
    1.18  
    1.19  
    1.20  (* local_qed *)