# HG changeset patch
# User ballarin
# Date 1221560825 -7200
# Node ID c447b60d67f593e745bb92527ea8e2e388b737df
# Parent  89e4d2232ed25151891439603dc79389f4c54d0d
Clearer separation of interpretation frontend and backend.

diff -r 89e4d2232ed2 -r c447b60d67f5 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Sep 16 12:26:15 2008 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Sep 16 12:27:05 2008 +0200
@@ -154,7 +154,7 @@
        Only required to generate the right witnesses for locales with predicates. *)
   elems: (Element.context_i * stamp) list,
     (* Static content, neither Fixes nor Constrains elements *)
-  params: ((string * typ) * mixfix) list,                             (*all params*)
+  params: ((string * typ) * mixfix) list,                        (*all term params*)
   decls: decl list * decl list,                    (*type/term_syntax declarations*)
   regs: ((string * string list) * Element.witness list) list,
     (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
@@ -202,18 +202,21 @@
 (** management of registrations in theories and proof contexts **)
 
 type registration =
-  {prfx: bool * string,
-      (* parameters and prefix
-       (if the Boolean flag is set, only accesses containing the prefix are generated,
-        otherwise the prefix may be omitted when accessing theorems etc.) *)
+  {prfx: (bool * string) * string,
+      (* first component: interpretation prefix;
+           if the Boolean flag is set, only accesses containing the prefix are generated,
+           otherwise the prefix may be omitted when accessing theorems etc.)
+         second component: parameter prefix *)
     exp: Morphism.morphism,
       (* maps content to its originating context *)
     imp: (typ Vartab.table * typ list) * (term Vartab.table * term list),
       (* inverse of exp *)
     wits: Element.witness list,
       (* witnesses of the registration *)
-    eqns: thm Termtab.table
+    eqns: thm Termtab.table,
       (* theorems (equations) interpreting derived concepts and indexed by lhs *)
+    morph: unit
+      (* interpreting morphism *)
   }
 
 structure Registrations :
@@ -223,34 +226,36 @@
     val join: T * T -> T
     val dest: theory -> T ->
       (term list *
-        ((bool * string) *
+        (((bool * string) * string) *
          (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) *
          Element.witness list *
          thm Termtab.table)) list
     val test: theory -> T * term list -> bool
     val lookup: theory ->
       T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
-      ((bool * string) * Element.witness list * thm Termtab.table) option
-    val insert: theory -> term list -> (bool * string) ->
+      (((bool * string) * string) * Element.witness list * thm Termtab.table) option
+    val insert: theory -> term list -> ((bool * string) * string) ->
       (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
       T ->
-      T * (term list * ((bool * string) * Element.witness list)) list
+      T * (term list * (((bool * string) * string) * Element.witness list)) list
     val add_witness: term list -> Element.witness -> T -> T
     val add_equation: term list -> thm -> T -> T
+(*    val update_morph: term list -> Element.witness list * thm list -> T -> T *)
+(*    val get_morph: theory -> T -> term list -> string list -> Morphism.morphism *)
   end =
 struct
   (* A registration is indexed by parameter instantiation.
      NB: index is exported whereas content is internalised. *)
   type T = registration Termtab.table;
 
-  fun mk_reg prfx exp imp wits eqns =
-    {prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns};
+  fun mk_reg prfx exp imp wits eqns morph =
+    {prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns, morph = morph};
 
   fun map_reg f reg =
     let
-      val {prfx, exp, imp, wits, eqns} = reg;
-      val (prfx', exp', imp', wits', eqns') = f (prfx, exp, imp, wits, eqns);
-    in mk_reg prfx' exp' imp' wits' eqns' end;
+      val {prfx, exp, imp, wits, eqns, morph} = reg;
+      val (prfx', exp', imp', wits', eqns', morph') = f (prfx, exp, imp, wits, eqns, morph);
+    in mk_reg prfx' exp' imp' wits' eqns' morph' end;
 
   val empty = Termtab.empty;
 
@@ -267,15 +272,15 @@
      - witnesses are equal, no attempt to subsumption testing;
      - union of equalities, if conflicting (i.e. two eqns with equal lhs)
        eqn of right theory takes precedence *)
-  fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {prfx = n, exp, imp, wits = w, eqns = e2}) =>
-      mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2))) (r1, r2);
+  fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {prfx = n, exp, imp, wits = w, eqns = e2, morph = m}) =>
+      mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2)) m) (r1, r2);
 
   fun dest_transfer thy regs =
-    Termtab.dest regs |> map (apsnd (map_reg (fn (n, e, i, ws, es) =>
-      (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es))));
+    Termtab.dest regs |> map (apsnd (map_reg (fn (n, e, i, ws, es, m) =>
+      (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es, m))));
 
   fun dest thy regs = dest_transfer thy regs |> map (apfst untermify) |>
-    map (apsnd (fn {prfx, exp, imp, wits, eqns} => (prfx, (exp, imp), wits, eqns)));
+    map (apsnd (fn {prfx, exp, imp, wits, eqns, ...} => (prfx, (exp, imp), wits, eqns)));
 
   (* registrations that subsume t *)
   fun subsumers thy t regs =
@@ -293,7 +298,7 @@
     in
       (case subs of
         [] => NONE
-        | ((t', {prfx, exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns}) :: _) =>
+        | ((t', {prfx, exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns, morph}) :: _) =>
           let
             val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
             val tinst' = domT' |> map (fn (T as TFree (x, _)) =>
@@ -320,7 +325,7 @@
                 val sups =
                   filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
                 val sups' = map (apfst untermify) sups |> map (fn (ts, {prfx, wits, ...}) => (ts, (prfx, wits)))
-              in (Termtab.update (t, mk_reg prfx exp imp [] Termtab.empty) regs, sups') end
+              in (Termtab.update (t, mk_reg prfx exp imp [] Termtab.empty ()) regs, sups') end
       | _ => (regs, []))
     end;
 
@@ -334,16 +339,26 @@
   (* add witness theorem to registration,
      only if instantiation is exact, otherwise exception Option raised *)
   fun add_witness ts wit regs =
-    gen_add (fn (x, e, i, wits, eqns) => (x, e, i, Element.close_witness wit :: wits, eqns))
+    gen_add (fn (x, e, i, wits, eqns, m) => (x, e, i, Element.close_witness wit :: wits, eqns, m))
       ts regs;
 
   (* add equation to registration, replaces previous equation with same lhs;
      only if instantiation is exact, otherwise exception Option raised;
      exception TERM raised if not a meta equality *)
   fun add_equation ts thm regs =
-    gen_add (fn (x, e, i, thms, eqns) =>
-      (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns))
+    gen_add (fn (x, e, i, thms, eqns, m) =>
+      (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns, m))
       ts regs;
+
+  (* update morphism of registration;
+     only if instantiation is exact, otherwise exception Option raised *)
+(*
+  fun update_morph ts (wits, eqns') regs =
+    gen_add (fn (x, e, i, thms, eqns, _) =>
+      (x, e, i, thms, eqns, (wits, eqns')))
+      ts regs;
+*)
+
 end;
 
 
@@ -456,12 +471,12 @@
 
 (* add registration to theory or context, ignored if subsumed *)
 
-fun put_registration (name, ps) prfx morphs (* wits *) ctxt =
+fun put_registration (name, ps) prfx morphs ctxt =
   RegistrationsData.map (fn regs =>
     let
       val thy = Context.theory_of ctxt;
       val reg = the_default Registrations.empty (Symtab.lookup regs name);
-      val (reg', sups) = Registrations.insert thy ps prfx morphs (* wits *) reg;
+      val (reg', sups) = Registrations.insert thy ps prfx morphs reg;
       val _ = if not (null sups) then warning
                 ("Subsumed interpretation(s) of locale " ^
                  quote (extern thy name) ^
@@ -506,6 +521,16 @@
 fun add_global_equation id thm = Context.theory_map (add_equation id thm);
 fun add_local_equation id thm = Context.proof_map (add_equation id thm);
 
+(*
+(* update morphism of registration, ignored if registration not present *)
+
+fun update_morph (name, ps) morph =
+  RegistrationsData.map (Symtab.map_entry name (Registrations.update_morph ps morph));
+
+fun update_global_morph id morph = Context.theory_map (update_morph id morph);
+fun update_local_morph id morph = Context.proof_map (update_morph id morph);
+*)
+
 
 (* printing of registrations *)
 
@@ -520,8 +545,8 @@
     val prt_thm = prt_term o prop_of;
     fun prt_inst ts =
         Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts));
-    fun prt_prfx (false, prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)"]
-      | prt_prfx (true, prfx) = [Pretty.str prfx];
+    fun prt_prfx ((false, prfx), pprfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)", Pretty.brk 1, Pretty.str pprfx]
+      | prt_prfx ((true, prfx), pprfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str pprfx];
     fun prt_eqns [] = Pretty.str "no equations."
       | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 ::
           Pretty.breaks (map prt_thm eqns));
@@ -622,8 +647,9 @@
   distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
 
 
+fun param_prefix params = space_implode "_" params;
 fun params_qualified params name =
-  NameSpace.qualified (space_implode "_" params) name;
+  NameSpace.qualified (param_prefix params) name;
 
 
 (* CB: param_types has the following type:
@@ -991,7 +1017,7 @@
               val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
             in if test_local_registration ctxt' (name, ps') then ctxt'
               else let
-                  val ctxt'' = put_local_registration (name, ps') (true, "")
+                  val ctxt'' = put_local_registration (name, ps') ((true, ""), "")
                     (Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt'
                 in case mode of
                     Assumed axs =>
@@ -1112,7 +1138,7 @@
     (* CB: fix of type bug of goal in target with context elements.
        Parameters new in context elements must receive types that are
        distinct from types of parameters in target (fixed_params).  *)
-    val ctxt_with_fixed =
+    val ctxt_with_fixed = 
       fold Variable.declare_term (map Free fixed_params) ctxt;
     val int_elemss =
       raw_elemss
@@ -1583,41 +1609,40 @@
 
 (* join equations of an id with already accumulated ones *)
 
-fun join_eqns get_reg prep_id ctxt id eqns =
+fun join_eqns get_reg id eqns =
   let
-    val id' = prep_id id
-    val eqns' = case get_reg id'
+    val eqns' = case get_reg id
       of NONE => eqns
-        | SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
-            handle Termtab.DUP t =>
-              error ("Conflicting interpreting equations for term " ^
-                quote (Syntax.string_of_term ctxt t))
-  in ((id', eqns'), eqns') end;
-
-
-(* collect witnesses and equations up to a particular target for global
+        | SOME (_, _, eqns') => Termtab.join (fn _ => fn (_, e) => e) (eqns, eqns')
+            (* prefer equations from eqns' *)
+  in ((id, eqns'), eqns') end;
+
+
+(* collect witnesses and equations up to a particular target for a
    registration; requires parameters and flattened list of identifiers
    instead of recomputing it from the target *)
 
-fun collect_global_witnesses thy imprt parms ids vts = let
-    val ts = map Logic.unvarify vts;
+fun collect_witnesses ctxt (imprt as ((impT, _), (imp, _))) parms ids ext_ts = let
+
+    val thy = ProofContext.theory_of ctxt;
+
+    val ts = map (var_inst_term (impT, imp)) ext_ts;
     val (parms, parmTs) = split_list parms;
     val parmvTs = map Logic.varifyT parmTs;
     val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
     val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
         |> Symtab.make;
-    (* replace parameter names in ids by instantiations *)
-    val vinst = Symtab.make (parms ~~ vts);
-    fun vinst_names ps = map (the o Symtab.lookup vinst) ps;
     val inst = Symtab.make (parms ~~ ts);
-    val inst_ids = map (apfst (apsnd vinst_names)) ids;
-    val assumed_ids' = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) inst_ids;
-    val wits = maps (#2 o the o get_global_registration thy imprt) assumed_ids';
-
-    val ids' = map fst inst_ids;
+
+    (* instantiate parameter names in ids *)
+    val ext_inst = Symtab.make (parms ~~ ext_ts);
+    fun ext_inst_names ps = map (the o Symtab.lookup ext_inst) ps;
+    val inst_ids = map (apfst (apsnd ext_inst_names)) ids;
+    val assumed_ids = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) inst_ids;
+    val wits = maps (#2 o the o get_local_registration ctxt imprt) assumed_ids;
     val eqns =
-      fold_map (join_eqns (get_global_registration thy imprt) I (ProofContext.init thy))
-        ids' Termtab.empty |> snd |> Termtab.dest |> map snd;
+      fold_map (join_eqns (get_local_registration ctxt imprt))
+        (map fst inst_ids) Termtab.empty |> snd |> Termtab.dest |> map snd;
   in ((tinst, inst), wits, eqns) end;
 
 
@@ -1646,18 +1671,16 @@
 
 (* compute morphism and apply to args *)
 
-fun interpret_args thy prfx insts prems eqns exp attrib args =
-  let
-    val inst = Morphism.name_morphism (Name.qualified prfx) $>
-(* need to add parameter prefix *) (* FIXME *)
-      Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
-      Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
-      Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns)
-  in
-    args |> Element.facts_map (morph_ctxt' inst) |>
-(* suppresses application of name morphism: workaroud for class package *) (* FIXME *)
-      standardize thy exp |> Attrib.map_facts attrib
-  end;
+fun inst_morph thy prfx param_prfx insts prems eqns =
+  Morphism.name_morphism (Name.qualified prfx o Name.qualified param_prfx) $>
+    Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
+    Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
+    Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns);
+
+fun interpret_args thy inst exp attrib args =
+  args |> Element.facts_map (morph_ctxt' inst) |>
+(* morph_ctxt' suppresses application of name morphism.  FIXME *)
+    standardize thy exp |> Attrib.map_facts attrib;
 
 
 (* store instantiations of args for all registered interpretations
@@ -1672,13 +1695,13 @@
     val regs = get_global_registrations thy target;
     (* add args to thy for all registrations *)
 
-    fun activate (vts, ((fully_qualified, prfx), (exp, imp), _, _)) thy =
+    fun activate (ext_ts, (((fully_qualified, prfx), pprfx), (exp, imp), _, _)) thy =
       let
-        val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts;
+        val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
         val attrib = Attrib.attribute_i thy;
         val args' = args
-          |> interpret_args thy prfx insts prems eqns exp attrib
-          |> add_param_prefixss (space_implode "_" (map fst parms));
+          |> interpret_args thy (inst_morph thy prfx pprfx insts prems eqns) exp attrib
+          |> add_param_prefixss pprfx;
       in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end;
   in fold activate regs thy end;
 
@@ -2046,27 +2069,26 @@
 
 (* activate instantiated facts in theory or context *)
 
-structure Idtab =
-  TableFun(type key = string * term list
-    val ord = prod_ord string_ord (list_ord Term.fast_term_ord));
-
-fun gen_activate_facts_elemss mk_ctxt get_reg note note_interp attrib put_reg test_reg add_wit add_eqn
-        prfx all_elemss propss eq_attns (exp, imp) thmss thy_ctxt =
+fun gen_activate_facts_elemss mk_ctxt note note_interp attrib put_reg add_wit add_eqn
+        prfx all_elemss pss propss eq_attns (exp, imp) thmss thy_ctxt =
   let
     val ctxt = mk_ctxt thy_ctxt;
+    fun get_reg thy_ctxt = get_local_registration (mk_ctxt thy_ctxt);
+    fun test_reg thy_ctxt = test_local_registration (mk_ctxt thy_ctxt);
+
     val (all_propss, eq_props) = chop (length all_elemss) propss;
     val (all_thmss, eq_thms) = chop (length all_elemss) thmss;
 
     (* Filter out fragments already registered. *)
 
     val (new_elemss, xs) = split_list (filter_out (fn (((id, _), _), _) =>
-          test_reg thy_ctxt id) (all_elemss ~~ (all_propss ~~ all_thmss)));
-    val (new_propss, new_thmss) = split_list xs;
+          test_reg thy_ctxt id) (all_elemss ~~ (pss ~~ (all_propss ~~ all_thmss))));
+    val (new_pss, ys) = split_list xs;
+    val (new_propss, new_thmss) = split_list ys;
 
     val thy_ctxt' = thy_ctxt
       (* add registrations *)
-(*      |> fold (fn ((id, _), _) => put_reg id prfx (exp, imp)) new_elemss *)
-      |> fold (fn (id, _) => put_reg id prfx (exp, imp)) new_propss
+      |> fold (fn (((id, _), _), ps) => put_reg id (prfx, param_prefix ps) (exp, imp)) (new_elemss ~~ new_pss)
       (* add witnesses of Assumed elements (only those generate proof obligations) *)
       |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst new_propss ~~ new_thmss)
       (* add equations *)
@@ -2078,66 +2100,64 @@
           (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id)
             | ((_, Derived _), _) => NONE) all_elemss);
 
-    fun activate_elem eqns loc (fully_qualified, prfx) (Notes (kind, facts)) thy_ctxt =
-        let
-          val ctxt = mk_ctxt thy_ctxt;
-          val facts' = interpret_args (ProofContext.theory_of ctxt) prfx
-              (Symtab.empty, Symtab.empty) prems eqns exp (attrib thy_ctxt) facts;
-        in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end
-      | activate_elem _ _ _ _ thy_ctxt = thy_ctxt;
-
-    fun activate_elems all_eqns ((id, _), elems) thy_ctxt =
-      let
-        val (prfx, _, _) = case get_reg thy_ctxt imp id
-         of SOME x => x
-          | NONE => sys_error ("Unknown registration of " ^ quote (fst id)
-              ^ " while activating facts.");
-      in fold (activate_elem (the (Idtab.lookup all_eqns id)) (fst id) prfx) elems thy_ctxt end;
-
     val thy_ctxt'' = thy_ctxt'
       (* add witnesses of Derived elements *)
       |> fold (fn (id, thms) => fold (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms)
          (map_filter (fn ((_, Assumed _), _) => NONE
             | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
 
-    (* Accumulate equations *)
-    val all_eqns =
-      fold_map (join_eqns (get_reg thy_ctxt'' imp) fst ctxt) all_propss Termtab.empty
-      |> fst
-      |> map (apsnd (map snd o Termtab.dest))
-      |> (fn xs => fold Idtab.update xs Idtab.empty)
-      (* Idtab.make wouldn't work here: can have conflicting duplicates,
-         because instantiation may equate ids and equations are accumulated! *)
+    fun activate_elem inst loc prfx pprfx (Notes (kind, facts)) thy_ctxt =
+        let
+          val ctxt = mk_ctxt thy_ctxt;
+          val facts' = facts |>
+              interpret_args (ProofContext.theory_of ctxt) inst exp (attrib thy_ctxt) |>
+              add_param_prefixss pprfx;
+        in snd (note_interp kind loc prfx facts' thy_ctxt) end
+      | activate_elem _ _ _ _ _ thy_ctxt = thy_ctxt;
+
+    fun activate_elems ((((loc, ext_ts), _), _), ps) thy_ctxt =
+      let
+        val ctxt = mk_ctxt thy_ctxt;
+        val thy = ProofContext.theory_of ctxt;
+        val {params, elems, ...} = the_locale thy loc;
+        val parms = map fst params;
+        val pprfx = param_prefix ps;
+        val ids = flatten (ProofContext.init thy, intern_expr thy)
+          (([], Symtab.empty), Expr (Locale loc)) |> fst |> fst;
+        val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts;
+        val inst = inst_morph thy (snd prfx) pprfx insts prems eqns;
+      in
+        fold (activate_elem inst loc prfx pprfx) (map fst elems) thy_ctxt
+      end;
 
   in
     thy_ctxt''
-    (* add equations *)
+    (* add equations as lemmas to context *)
     |> fold (fn (attns, thms) =>
          fold (fn (attn, thm) => note "lemma"
            [(apsnd (map (attrib thy_ctxt'')) attn,
              [([Element.conclude_witness thm], [])])] #> snd)
            (attns ~~ thms)) (unflat eq_thms eq_attns ~~ eq_thms)
-    (* add facts *)
-    |> fold (activate_elems all_eqns) new_elemss
+    (* add interpreted facts *)
+    |> fold activate_elems (new_elemss ~~ new_pss)
   end;
 
 fun global_activate_facts_elemss x = gen_activate_facts_elemss
       ProofContext.init
-      get_global_registration
       PureThy.note_thmss
       global_note_prefix_i
       Attrib.attribute_i
-      put_global_registration test_global_registration add_global_witness add_global_equation
+      put_global_registration
+      add_global_witness
+      add_global_equation
       x;
 
 fun local_activate_facts_elemss x = gen_activate_facts_elemss
       I
-      get_local_registration
       ProofContext.note_thmss_i
       local_note_prefix_i
       (Attrib.attribute_i o ProofContext.theory_of)
       put_local_registration
-      test_local_registration
       add_local_witness
       add_local_equation
       x;
@@ -2264,7 +2284,7 @@
 
     val propss = map extract_asms_elems inst_elemss @ eqn_elems;
 
-  in (propss, activate prfx inst_elemss propss eq_attns morphs) end;
+  in (propss, activate prfx inst_elemss (map (snd o fst) ids) propss eq_attns morphs) end;
 
 fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init
   test_global_registration
@@ -2323,11 +2343,11 @@
                 |> fold (add_witness_in_locale target id) thms
           | activate_id _ thy = thy;
 
-        fun activate_reg (vts, ((fully_qualified, prfx), (exp, imp), _, _)) thy =
+        fun activate_reg (ext_ts, (((fully_qualified, prfx), pprfx), (exp, imp), _, _)) thy =
           let
-            val (insts, wits, _) = collect_global_witnesses thy imp fixed target_ids vts;
+            val (insts, wits, _) = collect_witnesses (ProofContext.init thy) imp fixed target_ids ext_ts;
             fun inst_parms ps = map
-                  (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps;
+                  (the o AList.lookup (op =) (map #1 fixed ~~ ext_ts)) ps;
             val disch = Element.satisfy_thm wits;
             val new_elemss = filter (fn (((name, ps), _), _) =>
                 not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
@@ -2338,7 +2358,7 @@
                 if test_global_registration thy (name, ps')
                 then thy
                 else thy
-                  |> put_global_registration (name, ps') (fully_qualified, prfx) (exp, imp)
+                  |> put_global_registration (name, ps') ((fully_qualified, prfx), param_prefix ps) (exp, imp)
                   |> fold (fn witn => fn thy => add_global_witness (name, ps')
                      (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms
               end;
@@ -2350,7 +2370,7 @@
                 if test_global_registration thy (name, ps')
                 then thy
                 else thy
-                  |> put_global_registration (name, ps') (fully_qualified, prfx) (exp, imp)
+                  |> put_global_registration (name, ps') ((fully_qualified, prfx), param_prefix ps) (exp, imp)
                   |> fold (fn witn => fn thy => add_global_witness (name, ps')
                        (witn |> Element.map_witness (fn (t, th) =>  (* FIXME *)
                        (Element.inst_term insts t,
@@ -2361,6 +2381,7 @@
                 let
                   val att_morphism =
                     Morphism.name_morphism (Name.qualified prfx) $>
+(* FIXME? treatment of parameter prefix *)
                     Morphism.thm_morphism satisfy $>
                     Element.inst_morphism thy insts $>
                     Morphism.thm_morphism disch;