more careful treatment position: existing facts refer to interpretation command, future facts refer to themselves (see also 4270da306442);
authorwenzelm
Thu Aug 30 14:48:02 2018 +0200 (13 months ago)
changeset 6885559ce31e15c33
parent 68854 404e04f649d4
child 68856 e5097a5b2e58
more careful treatment position: existing facts refer to interpretation command, future facts refer to themselves (see also 4270da306442);
src/Pure/Isar/interpretation.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/interpretation.ML	Thu Aug 30 14:38:24 2018 +0200
     1.2 +++ b/src/Pure/Isar/interpretation.ML	Thu Aug 30 14:48:02 2018 +0200
     1.3 @@ -100,7 +100,7 @@
     1.4  fun abs_def_rule eqns ctxt =
     1.5    (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt);
     1.6  
     1.7 -fun note_eqns_register pos note add_registration
     1.8 +fun note_eqns_register note add_registration
     1.9      deps eqnss witss def_eqns thms export export' ctxt =
    1.10    let
    1.11      val factss = thms
    1.12 @@ -112,10 +112,7 @@
    1.13      val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule;
    1.14      val deps' =
    1.15        (deps ~~ witss) |> map (fn ((dep, morph), wits) =>
    1.16 -        let val morph' = morph
    1.17 -          $> Element.satisfy_morphism (map (Element.transform_witness export') wits)
    1.18 -          $> Morphism.binding_morphism "position" (Binding.set_pos pos)
    1.19 -        in (dep, morph') end);
    1.20 +        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)));
    1.21      fun register (dep, eqns) ctxt =
    1.22        ctxt |> add_registration
    1.23          {dep = dep,
    1.24 @@ -132,9 +129,8 @@
    1.25    let
    1.26      val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) =
    1.27        prep_interpretation expression raw_defs initial_ctxt;
    1.28 -    val pos = Position.thread_data ();
    1.29      fun after_qed witss eqns =
    1.30 -      note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns export export';
    1.31 +      note_eqns_register note add_registration deps eqnss witss def_eqns eqns export export';
    1.32    in setup_proof after_qed propss (flat eq_propss) goal_ctxt end;
    1.33  
    1.34  end;
     2.1 --- a/src/Pure/Isar/locale.ML	Thu Aug 30 14:38:24 2018 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Thu Aug 30 14:48:02 2018 +0200
     2.3 @@ -542,6 +542,7 @@
     2.4  fun add_registration {dep = (name, base_morph), mixin, export} context =
     2.5    let
     2.6      val thy = Context.theory_of context;
     2.7 +    val pos_morph = Morphism.binding_morphism "position" (Binding.set_pos (Position.thread_data ()));
     2.8      val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
     2.9      val morph = base_morph $> mix;
    2.10      val inst = instance_of thy name morph;
    2.11 @@ -557,7 +558,7 @@
    2.12        (* add mixin *)
    2.13        |> amend_registration {dep = (name, morph), mixin = mixin, export = export}
    2.14        (* activate import hierarchy as far as not already active *)
    2.15 -      |> activate_facts (SOME export) (name, morph)
    2.16 +      |> activate_facts (SOME export) (name, morph $> pos_morph)
    2.17    end;
    2.18  
    2.19  val add_registration_theory = Context.theory_map o add_registration;