src/Pure/Isar/expression.ML
changeset 38757 2b3e054ae6fc
parent 38756 d07959fabde6
child 39288 f1ae2493d93f
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Aug 26 13:09:12 2010 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Aug 26 15:48:08 2010 +0200
     1.3 @@ -824,8 +824,9 @@
     1.4      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
     1.5      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
     1.6  
     1.7 -    fun after_qed witss eqns = (ProofContext.background_theory o Context.theory_map)
     1.8 -      (note_eqns_register deps witss attrss eqns export export');
     1.9 +    fun after_qed witss eqns =
    1.10 +      (ProofContext.background_theory o Context.theory_map)
    1.11 +        (note_eqns_register deps witss attrss eqns export export');
    1.12  
    1.13    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
    1.14