src/Pure/Isar/expression.ML
changeset 57860 bcc243ea48e7
parent 57181 2d13bf9ea77b
child 57926 59b2572e8e93
     1.1 --- a/src/Pure/Isar/expression.ML	Tue Aug 05 12:01:32 2014 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Tue Aug 05 12:14:25 2014 +0200
     1.3 @@ -865,8 +865,8 @@
     1.4  
     1.5  (* generic interpretation machinery *)
     1.6  
     1.7 -fun meta_rewrite eqns ctxt =
     1.8 -  (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
     1.9 +fun meta_rewrite ctxt eqns =
    1.10 +  map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns);
    1.11  
    1.12  fun note_eqns_register note activate deps witss eqns attrss export export' ctxt =
    1.13    let
    1.14 @@ -874,7 +874,7 @@
    1.15        (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns;
    1.16      val (eqns', ctxt') = ctxt
    1.17        |> note Thm.lemmaK facts
    1.18 -      |-> meta_rewrite;
    1.19 +      |> (fn (eqns, ctxt') => (meta_rewrite ctxt' eqns, ctxt'));
    1.20      val dep_morphs =
    1.21        map2 (fn (dep, morph) => fn wits =>
    1.22            (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)))