# HG changeset patch
# User wenzelm
# Date 1407233665 -7200
# Node ID bcc243ea48e7967824470c1d670587324f11a595
# Parent  29e728588163b5fa467cf99f33ce49223821021b
tuned;

diff -r 29e728588163 -r bcc243ea48e7 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Aug 05 12:01:32 2014 +0200
+++ b/src/Pure/Isar/expression.ML	Tue Aug 05 12:14:25 2014 +0200
@@ -865,8 +865,8 @@
 
 (* generic interpretation machinery *)
 
-fun meta_rewrite eqns ctxt =
-  (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
+fun meta_rewrite ctxt eqns =
+  map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns);
 
 fun note_eqns_register note activate deps witss eqns attrss export export' ctxt =
   let
@@ -874,7 +874,7 @@
       (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
     val (eqns', ctxt') = ctxt
       |> note Thm.lemmaK facts
-      |-> meta_rewrite;
+      |> (fn (eqns, ctxt') => (meta_rewrite ctxt' eqns, ctxt'));
     val dep_morphs =
       map2 (fn (dep, morph) => fn wits =>
           (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)))