src/Pure/Isar/expression.ML
changeset 46899 58110c1e02bc
parent 46858 05f30c796f95
child 46922 3717f3878714
     1.1 --- a/src/Pure/Isar/expression.ML	Tue Mar 13 13:31:26 2012 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Tue Mar 13 14:17:42 2012 +0100
     1.3 @@ -858,7 +858,8 @@
     1.4  
     1.5      fun after_qed witss eqns =
     1.6        (Proof.map_context o Context.proof_map)
     1.7 -        (note_eqns_register deps witss attrss eqns export export');
     1.8 +        (note_eqns_register deps witss attrss eqns export export')
     1.9 +      #> Proof.put_facts NONE;
    1.10    in
    1.11      state
    1.12      |> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int