src/Pure/Isar/interpretation.ML
changeset 68854 404e04f649d4
parent 68852 becaeaa334ae
child 68855 59ce31e15c33
     1.1 --- a/src/Pure/Isar/interpretation.ML	Thu Aug 30 14:21:40 2018 +0200
     1.2 +++ b/src/Pure/Isar/interpretation.ML	Thu Aug 30 14:38:24 2018 +0200
     1.3 @@ -97,7 +97,7 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun meta_rewrite eqns ctxt =
     1.8 +fun abs_def_rule eqns ctxt =
     1.9    (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt);
    1.10  
    1.11  fun note_eqns_register pos note add_registration
    1.12 @@ -107,25 +107,23 @@
    1.13        |> unflat ((map o map) #1 eqnss)
    1.14        |> map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) #1 eqnss);
    1.15      val (eqnss', ctxt') =
    1.16 -      fold_map (fn facts => note Thm.theoremK facts #-> meta_rewrite) factss ctxt;
    1.17 +      fold_map (fn facts => note Thm.theoremK facts #-> abs_def_rule) factss ctxt;
    1.18      val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]);
    1.19 -    val (eqns', ctxt'') = ctxt'
    1.20 -      |> note Thm.theoremK [defs]
    1.21 -      |-> meta_rewrite;
    1.22 -    val dep_morphs =
    1.23 -      map2 (fn (dep, morph) => fn wits =>
    1.24 +    val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule;
    1.25 +    val deps' =
    1.26 +      (deps ~~ witss) |> map (fn ((dep, morph), wits) =>
    1.27          let val morph' = morph
    1.28            $> Element.satisfy_morphism (map (Element.transform_witness export') wits)
    1.29            $> Morphism.binding_morphism "position" (Binding.set_pos pos)
    1.30 -        in (dep, morph') end) deps witss;
    1.31 -    fun register (dep_morph, eqns) ctxt =
    1.32 +        in (dep, morph') end);
    1.33 +    fun register (dep, eqns) ctxt =
    1.34        ctxt |> add_registration
    1.35 -        {dep = dep_morph,
    1.36 +        {dep = dep,
    1.37            mixin =
    1.38              Option.map (rpair true)
    1.39                (Element.eq_morphism (Proof_Context.theory_of ctxt) (eqns @ eqns')),
    1.40            export = export};
    1.41 -  in ctxt'' |> fold register (dep_morphs ~~ eqnss') end;
    1.42 +  in ctxt'' |> fold register (deps' ~~ eqnss') end;
    1.43  
    1.44  in
    1.45