--- a/src/Pure/Isar/expression.ML Thu Aug 26 13:09:12 2010 +0200
+++ b/src/Pure/Isar/expression.ML Thu Aug 26 15:48:08 2010 +0200
@@ -824,8 +824,9 @@
val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
val export' = Variable.export_morphism goal_ctxt expr_ctxt;
- fun after_qed witss eqns = (ProofContext.background_theory o Context.theory_map)
- (note_eqns_register deps witss attrss eqns export export');
+ fun after_qed witss eqns =
+ (ProofContext.background_theory o Context.theory_map)
+ (note_eqns_register deps witss attrss eqns export export');
in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;