# HG changeset patch # User wenzelm # Date 1535633282 -7200 # Node ID 59ce31e15c33c7c54516b72c8b219072bdb31f35 # Parent 404e04f649d4cdabf92cfb77e7c1a61a7bee0e60 more careful treatment position: existing facts refer to interpretation command, future facts refer to themselves (see also 4270da306442); diff -r 404e04f649d4 -r 59ce31e15c33 src/Pure/Isar/interpretation.ML --- a/src/Pure/Isar/interpretation.ML Thu Aug 30 14:38:24 2018 +0200 +++ b/src/Pure/Isar/interpretation.ML Thu Aug 30 14:48:02 2018 +0200 @@ -100,7 +100,7 @@ fun abs_def_rule eqns ctxt = (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt); -fun note_eqns_register pos note add_registration +fun note_eqns_register note add_registration deps eqnss witss def_eqns thms export export' ctxt = let val factss = thms @@ -112,10 +112,7 @@ val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule; val deps' = (deps ~~ witss) |> map (fn ((dep, morph), wits) => - let val morph' = morph - $> Element.satisfy_morphism (map (Element.transform_witness export') wits) - $> Morphism.binding_morphism "position" (Binding.set_pos pos) - in (dep, morph') end); + (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))); fun register (dep, eqns) ctxt = ctxt |> add_registration {dep = dep, @@ -132,9 +129,8 @@ let val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) = prep_interpretation expression raw_defs initial_ctxt; - val pos = Position.thread_data (); fun after_qed witss eqns = - note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns export export'; + note_eqns_register note add_registration deps eqnss witss def_eqns eqns export export'; in setup_proof after_qed propss (flat eq_propss) goal_ctxt end; end; diff -r 404e04f649d4 -r 59ce31e15c33 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Aug 30 14:38:24 2018 +0200 +++ b/src/Pure/Isar/locale.ML Thu Aug 30 14:48:02 2018 +0200 @@ -542,6 +542,7 @@ fun add_registration {dep = (name, base_morph), mixin, export} context = let val thy = Context.theory_of context; + val pos_morph = Morphism.binding_morphism "position" (Binding.set_pos (Position.thread_data ())); val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix); val morph = base_morph $> mix; val inst = instance_of thy name morph; @@ -557,7 +558,7 @@ (* add mixin *) |> amend_registration {dep = (name, morph), mixin = mixin, export = export} (* activate import hierarchy as far as not already active *) - |> activate_facts (SOME export) (name, morph) + |> activate_facts (SOME export) (name, morph $> pos_morph) end; val add_registration_theory = Context.theory_map o add_registration;