src/Pure/Isar/expression.ML
changeset 47068 2027ff3136cc
parent 46922 3717f3878714
child 47249 c0481c3c2a6c
     1.1 --- a/src/Pure/Isar/expression.ML	Wed Mar 21 21:06:31 2012 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Mar 21 21:24:13 2012 +0100
     1.3 @@ -860,7 +860,7 @@
     1.4      fun after_qed witss eqns =
     1.5        (Proof.map_context o Context.proof_map)
     1.6          (note_eqns_register deps witss attrss eqns export export')
     1.7 -      #> Proof.put_facts NONE;
     1.8 +      #> Proof.reset_facts;
     1.9    in
    1.10      state
    1.11      |> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int