Clearer separation of interpretation frontend and backend.
authorballarin
Tue Sep 16 12:27:05 2008 +0200 (2008-09-16)
changeset 28236c447b60d67f5
parent 28235 89e4d2232ed2
child 28237 f1fc11c73569
Clearer separation of interpretation frontend and backend.
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Tue Sep 16 12:26:15 2008 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Tue Sep 16 12:27:05 2008 +0200
     1.3 @@ -154,7 +154,7 @@
     1.4         Only required to generate the right witnesses for locales with predicates. *)
     1.5    elems: (Element.context_i * stamp) list,
     1.6      (* Static content, neither Fixes nor Constrains elements *)
     1.7 -  params: ((string * typ) * mixfix) list,                             (*all params*)
     1.8 +  params: ((string * typ) * mixfix) list,                        (*all term params*)
     1.9    decls: decl list * decl list,                    (*type/term_syntax declarations*)
    1.10    regs: ((string * string list) * Element.witness list) list,
    1.11      (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
    1.12 @@ -202,18 +202,21 @@
    1.13  (** management of registrations in theories and proof contexts **)
    1.14  
    1.15  type registration =
    1.16 -  {prfx: bool * string,
    1.17 -      (* parameters and prefix
    1.18 -       (if the Boolean flag is set, only accesses containing the prefix are generated,
    1.19 -        otherwise the prefix may be omitted when accessing theorems etc.) *)
    1.20 +  {prfx: (bool * string) * string,
    1.21 +      (* first component: interpretation prefix;
    1.22 +           if the Boolean flag is set, only accesses containing the prefix are generated,
    1.23 +           otherwise the prefix may be omitted when accessing theorems etc.)
    1.24 +         second component: parameter prefix *)
    1.25      exp: Morphism.morphism,
    1.26        (* maps content to its originating context *)
    1.27      imp: (typ Vartab.table * typ list) * (term Vartab.table * term list),
    1.28        (* inverse of exp *)
    1.29      wits: Element.witness list,
    1.30        (* witnesses of the registration *)
    1.31 -    eqns: thm Termtab.table
    1.32 +    eqns: thm Termtab.table,
    1.33        (* theorems (equations) interpreting derived concepts and indexed by lhs *)
    1.34 +    morph: unit
    1.35 +      (* interpreting morphism *)
    1.36    }
    1.37  
    1.38  structure Registrations :
    1.39 @@ -223,34 +226,36 @@
    1.40      val join: T * T -> T
    1.41      val dest: theory -> T ->
    1.42        (term list *
    1.43 -        ((bool * string) *
    1.44 +        (((bool * string) * string) *
    1.45           (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) *
    1.46           Element.witness list *
    1.47           thm Termtab.table)) list
    1.48      val test: theory -> T * term list -> bool
    1.49      val lookup: theory ->
    1.50        T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
    1.51 -      ((bool * string) * Element.witness list * thm Termtab.table) option
    1.52 -    val insert: theory -> term list -> (bool * string) ->
    1.53 +      (((bool * string) * string) * Element.witness list * thm Termtab.table) option
    1.54 +    val insert: theory -> term list -> ((bool * string) * string) ->
    1.55        (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
    1.56        T ->
    1.57 -      T * (term list * ((bool * string) * Element.witness list)) list
    1.58 +      T * (term list * (((bool * string) * string) * Element.witness list)) list
    1.59      val add_witness: term list -> Element.witness -> T -> T
    1.60      val add_equation: term list -> thm -> T -> T
    1.61 +(*    val update_morph: term list -> Element.witness list * thm list -> T -> T *)
    1.62 +(*    val get_morph: theory -> T -> term list -> string list -> Morphism.morphism *)
    1.63    end =
    1.64  struct
    1.65    (* A registration is indexed by parameter instantiation.
    1.66       NB: index is exported whereas content is internalised. *)
    1.67    type T = registration Termtab.table;
    1.68  
    1.69 -  fun mk_reg prfx exp imp wits eqns =
    1.70 -    {prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns};
    1.71 +  fun mk_reg prfx exp imp wits eqns morph =
    1.72 +    {prfx = prfx, exp = exp, imp = imp, wits = wits, eqns = eqns, morph = morph};
    1.73  
    1.74    fun map_reg f reg =
    1.75      let
    1.76 -      val {prfx, exp, imp, wits, eqns} = reg;
    1.77 -      val (prfx', exp', imp', wits', eqns') = f (prfx, exp, imp, wits, eqns);
    1.78 -    in mk_reg prfx' exp' imp' wits' eqns' end;
    1.79 +      val {prfx, exp, imp, wits, eqns, morph} = reg;
    1.80 +      val (prfx', exp', imp', wits', eqns', morph') = f (prfx, exp, imp, wits, eqns, morph);
    1.81 +    in mk_reg prfx' exp' imp' wits' eqns' morph' end;
    1.82  
    1.83    val empty = Termtab.empty;
    1.84  
    1.85 @@ -267,15 +272,15 @@
    1.86       - witnesses are equal, no attempt to subsumption testing;
    1.87       - union of equalities, if conflicting (i.e. two eqns with equal lhs)
    1.88         eqn of right theory takes precedence *)
    1.89 -  fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {prfx = n, exp, imp, wits = w, eqns = e2}) =>
    1.90 -      mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2))) (r1, r2);
    1.91 +  fun join (r1, r2) = Termtab.join (fn _ => fn ({eqns = e1, ...}, {prfx = n, exp, imp, wits = w, eqns = e2, morph = m}) =>
    1.92 +      mk_reg n exp imp w (Termtab.join (fn _ => fn (_, e) => e) (e1, e2)) m) (r1, r2);
    1.93  
    1.94    fun dest_transfer thy regs =
    1.95 -    Termtab.dest regs |> map (apsnd (map_reg (fn (n, e, i, ws, es) =>
    1.96 -      (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es))));
    1.97 +    Termtab.dest regs |> map (apsnd (map_reg (fn (n, e, i, ws, es, m) =>
    1.98 +      (n, e, i, map (Element.transfer_witness thy) ws, Termtab.map (transfer thy) es, m))));
    1.99  
   1.100    fun dest thy regs = dest_transfer thy regs |> map (apfst untermify) |>
   1.101 -    map (apsnd (fn {prfx, exp, imp, wits, eqns} => (prfx, (exp, imp), wits, eqns)));
   1.102 +    map (apsnd (fn {prfx, exp, imp, wits, eqns, ...} => (prfx, (exp, imp), wits, eqns)));
   1.103  
   1.104    (* registrations that subsume t *)
   1.105    fun subsumers thy t regs =
   1.106 @@ -293,7 +298,7 @@
   1.107      in
   1.108        (case subs of
   1.109          [] => NONE
   1.110 -        | ((t', {prfx, exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns}) :: _) =>
   1.111 +        | ((t', {prfx, exp = exp', imp = ((impT', domT'), (imp', dom')), wits, eqns, morph}) :: _) =>
   1.112            let
   1.113              val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
   1.114              val tinst' = domT' |> map (fn (T as TFree (x, _)) =>
   1.115 @@ -320,7 +325,7 @@
   1.116                  val sups =
   1.117                    filter (fn (t', _) => Pattern.matches thy (t, t')) (dest_transfer thy regs);
   1.118                  val sups' = map (apfst untermify) sups |> map (fn (ts, {prfx, wits, ...}) => (ts, (prfx, wits)))
   1.119 -              in (Termtab.update (t, mk_reg prfx exp imp [] Termtab.empty) regs, sups') end
   1.120 +              in (Termtab.update (t, mk_reg prfx exp imp [] Termtab.empty ()) regs, sups') end
   1.121        | _ => (regs, []))
   1.122      end;
   1.123  
   1.124 @@ -334,16 +339,26 @@
   1.125    (* add witness theorem to registration,
   1.126       only if instantiation is exact, otherwise exception Option raised *)
   1.127    fun add_witness ts wit regs =
   1.128 -    gen_add (fn (x, e, i, wits, eqns) => (x, e, i, Element.close_witness wit :: wits, eqns))
   1.129 +    gen_add (fn (x, e, i, wits, eqns, m) => (x, e, i, Element.close_witness wit :: wits, eqns, m))
   1.130        ts regs;
   1.131  
   1.132    (* add equation to registration, replaces previous equation with same lhs;
   1.133       only if instantiation is exact, otherwise exception Option raised;
   1.134       exception TERM raised if not a meta equality *)
   1.135    fun add_equation ts thm regs =
   1.136 -    gen_add (fn (x, e, i, thms, eqns) =>
   1.137 -      (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns))
   1.138 +    gen_add (fn (x, e, i, thms, eqns, m) =>
   1.139 +      (x, e, i, thms, Termtab.update (thm |> prop_of |> Logic.dest_equals |> fst, Thm.close_derivation thm) eqns, m))
   1.140        ts regs;
   1.141 +
   1.142 +  (* update morphism of registration;
   1.143 +     only if instantiation is exact, otherwise exception Option raised *)
   1.144 +(*
   1.145 +  fun update_morph ts (wits, eqns') regs =
   1.146 +    gen_add (fn (x, e, i, thms, eqns, _) =>
   1.147 +      (x, e, i, thms, eqns, (wits, eqns')))
   1.148 +      ts regs;
   1.149 +*)
   1.150 +
   1.151  end;
   1.152  
   1.153  
   1.154 @@ -456,12 +471,12 @@
   1.155  
   1.156  (* add registration to theory or context, ignored if subsumed *)
   1.157  
   1.158 -fun put_registration (name, ps) prfx morphs (* wits *) ctxt =
   1.159 +fun put_registration (name, ps) prfx morphs ctxt =
   1.160    RegistrationsData.map (fn regs =>
   1.161      let
   1.162        val thy = Context.theory_of ctxt;
   1.163        val reg = the_default Registrations.empty (Symtab.lookup regs name);
   1.164 -      val (reg', sups) = Registrations.insert thy ps prfx morphs (* wits *) reg;
   1.165 +      val (reg', sups) = Registrations.insert thy ps prfx morphs reg;
   1.166        val _ = if not (null sups) then warning
   1.167                  ("Subsumed interpretation(s) of locale " ^
   1.168                   quote (extern thy name) ^
   1.169 @@ -506,6 +521,16 @@
   1.170  fun add_global_equation id thm = Context.theory_map (add_equation id thm);
   1.171  fun add_local_equation id thm = Context.proof_map (add_equation id thm);
   1.172  
   1.173 +(*
   1.174 +(* update morphism of registration, ignored if registration not present *)
   1.175 +
   1.176 +fun update_morph (name, ps) morph =
   1.177 +  RegistrationsData.map (Symtab.map_entry name (Registrations.update_morph ps morph));
   1.178 +
   1.179 +fun update_global_morph id morph = Context.theory_map (update_morph id morph);
   1.180 +fun update_local_morph id morph = Context.proof_map (update_morph id morph);
   1.181 +*)
   1.182 +
   1.183  
   1.184  (* printing of registrations *)
   1.185  
   1.186 @@ -520,8 +545,8 @@
   1.187      val prt_thm = prt_term o prop_of;
   1.188      fun prt_inst ts =
   1.189          Pretty.enclose "(" ")" (Pretty.breaks (map prt_term' ts));
   1.190 -    fun prt_prfx (false, prfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)"]
   1.191 -      | prt_prfx (true, prfx) = [Pretty.str prfx];
   1.192 +    fun prt_prfx ((false, prfx), pprfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str "(optional)", Pretty.brk 1, Pretty.str pprfx]
   1.193 +      | prt_prfx ((true, prfx), pprfx) = [Pretty.str prfx, Pretty.brk 1, Pretty.str pprfx];
   1.194      fun prt_eqns [] = Pretty.str "no equations."
   1.195        | prt_eqns eqns = Pretty.block (Pretty.str "equations:" :: Pretty.brk 1 ::
   1.196            Pretty.breaks (map prt_thm eqns));
   1.197 @@ -622,8 +647,9 @@
   1.198    distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
   1.199  
   1.200  
   1.201 +fun param_prefix params = space_implode "_" params;
   1.202  fun params_qualified params name =
   1.203 -  NameSpace.qualified (space_implode "_" params) name;
   1.204 +  NameSpace.qualified (param_prefix params) name;
   1.205  
   1.206  
   1.207  (* CB: param_types has the following type:
   1.208 @@ -991,7 +1017,7 @@
   1.209                val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
   1.210              in if test_local_registration ctxt' (name, ps') then ctxt'
   1.211                else let
   1.212 -                  val ctxt'' = put_local_registration (name, ps') (true, "")
   1.213 +                  val ctxt'' = put_local_registration (name, ps') ((true, ""), "")
   1.214                      (Morphism.identity, ((Vartab.empty, []), (Vartab.empty, []) )) ctxt'
   1.215                  in case mode of
   1.216                      Assumed axs =>
   1.217 @@ -1112,7 +1138,7 @@
   1.218      (* CB: fix of type bug of goal in target with context elements.
   1.219         Parameters new in context elements must receive types that are
   1.220         distinct from types of parameters in target (fixed_params).  *)
   1.221 -    val ctxt_with_fixed =
   1.222 +    val ctxt_with_fixed = 
   1.223        fold Variable.declare_term (map Free fixed_params) ctxt;
   1.224      val int_elemss =
   1.225        raw_elemss
   1.226 @@ -1583,41 +1609,40 @@
   1.227  
   1.228  (* join equations of an id with already accumulated ones *)
   1.229  
   1.230 -fun join_eqns get_reg prep_id ctxt id eqns =
   1.231 +fun join_eqns get_reg id eqns =
   1.232    let
   1.233 -    val id' = prep_id id
   1.234 -    val eqns' = case get_reg id'
   1.235 +    val eqns' = case get_reg id
   1.236        of NONE => eqns
   1.237 -        | SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
   1.238 -            handle Termtab.DUP t =>
   1.239 -              error ("Conflicting interpreting equations for term " ^
   1.240 -                quote (Syntax.string_of_term ctxt t))
   1.241 -  in ((id', eqns'), eqns') end;
   1.242 -
   1.243 -
   1.244 -(* collect witnesses and equations up to a particular target for global
   1.245 +        | SOME (_, _, eqns') => Termtab.join (fn _ => fn (_, e) => e) (eqns, eqns')
   1.246 +            (* prefer equations from eqns' *)
   1.247 +  in ((id, eqns'), eqns') end;
   1.248 +
   1.249 +
   1.250 +(* collect witnesses and equations up to a particular target for a
   1.251     registration; requires parameters and flattened list of identifiers
   1.252     instead of recomputing it from the target *)
   1.253  
   1.254 -fun collect_global_witnesses thy imprt parms ids vts = let
   1.255 -    val ts = map Logic.unvarify vts;
   1.256 +fun collect_witnesses ctxt (imprt as ((impT, _), (imp, _))) parms ids ext_ts = let
   1.257 +
   1.258 +    val thy = ProofContext.theory_of ctxt;
   1.259 +
   1.260 +    val ts = map (var_inst_term (impT, imp)) ext_ts;
   1.261      val (parms, parmTs) = split_list parms;
   1.262      val parmvTs = map Logic.varifyT parmTs;
   1.263      val vtinst = fold (Sign.typ_match thy) (parmvTs ~~ map Term.fastype_of ts) Vartab.empty;
   1.264      val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T))
   1.265          |> Symtab.make;
   1.266 -    (* replace parameter names in ids by instantiations *)
   1.267 -    val vinst = Symtab.make (parms ~~ vts);
   1.268 -    fun vinst_names ps = map (the o Symtab.lookup vinst) ps;
   1.269      val inst = Symtab.make (parms ~~ ts);
   1.270 -    val inst_ids = map (apfst (apsnd vinst_names)) ids;
   1.271 -    val assumed_ids' = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) inst_ids;
   1.272 -    val wits = maps (#2 o the o get_global_registration thy imprt) assumed_ids';
   1.273 -
   1.274 -    val ids' = map fst inst_ids;
   1.275 +
   1.276 +    (* instantiate parameter names in ids *)
   1.277 +    val ext_inst = Symtab.make (parms ~~ ext_ts);
   1.278 +    fun ext_inst_names ps = map (the o Symtab.lookup ext_inst) ps;
   1.279 +    val inst_ids = map (apfst (apsnd ext_inst_names)) ids;
   1.280 +    val assumed_ids = map_filter (fn (id, (_, Assumed _)) => SOME id | _ => NONE) inst_ids;
   1.281 +    val wits = maps (#2 o the o get_local_registration ctxt imprt) assumed_ids;
   1.282      val eqns =
   1.283 -      fold_map (join_eqns (get_global_registration thy imprt) I (ProofContext.init thy))
   1.284 -        ids' Termtab.empty |> snd |> Termtab.dest |> map snd;
   1.285 +      fold_map (join_eqns (get_local_registration ctxt imprt))
   1.286 +        (map fst inst_ids) Termtab.empty |> snd |> Termtab.dest |> map snd;
   1.287    in ((tinst, inst), wits, eqns) end;
   1.288  
   1.289  
   1.290 @@ -1646,18 +1671,16 @@
   1.291  
   1.292  (* compute morphism and apply to args *)
   1.293  
   1.294 -fun interpret_args thy prfx insts prems eqns exp attrib args =
   1.295 -  let
   1.296 -    val inst = Morphism.name_morphism (Name.qualified prfx) $>
   1.297 -(* need to add parameter prefix *) (* FIXME *)
   1.298 -      Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
   1.299 -      Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
   1.300 -      Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns)
   1.301 -  in
   1.302 -    args |> Element.facts_map (morph_ctxt' inst) |>
   1.303 -(* suppresses application of name morphism: workaroud for class package *) (* FIXME *)
   1.304 -      standardize thy exp |> Attrib.map_facts attrib
   1.305 -  end;
   1.306 +fun inst_morph thy prfx param_prfx insts prems eqns =
   1.307 +  Morphism.name_morphism (Name.qualified prfx o Name.qualified param_prfx) $>
   1.308 +    Element.inst_morphism thy insts $> Element.satisfy_morphism prems $>
   1.309 +    Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
   1.310 +    Morphism.thm_morphism (MetaSimplifier.rewrite_rule eqns);
   1.311 +
   1.312 +fun interpret_args thy inst exp attrib args =
   1.313 +  args |> Element.facts_map (morph_ctxt' inst) |>
   1.314 +(* morph_ctxt' suppresses application of name morphism.  FIXME *)
   1.315 +    standardize thy exp |> Attrib.map_facts attrib;
   1.316  
   1.317  
   1.318  (* store instantiations of args for all registered interpretations
   1.319 @@ -1672,13 +1695,13 @@
   1.320      val regs = get_global_registrations thy target;
   1.321      (* add args to thy for all registrations *)
   1.322  
   1.323 -    fun activate (vts, ((fully_qualified, prfx), (exp, imp), _, _)) thy =
   1.324 +    fun activate (ext_ts, (((fully_qualified, prfx), pprfx), (exp, imp), _, _)) thy =
   1.325        let
   1.326 -        val (insts, prems, eqns) = collect_global_witnesses thy imp parms ids vts;
   1.327 +        val (insts, prems, eqns) = collect_witnesses (ProofContext.init thy) imp parms ids ext_ts;
   1.328          val attrib = Attrib.attribute_i thy;
   1.329          val args' = args
   1.330 -          |> interpret_args thy prfx insts prems eqns exp attrib
   1.331 -          |> add_param_prefixss (space_implode "_" (map fst parms));
   1.332 +          |> interpret_args thy (inst_morph thy prfx pprfx insts prems eqns) exp attrib
   1.333 +          |> add_param_prefixss pprfx;
   1.334        in global_note_prefix_i kind target (fully_qualified, prfx) args' thy |> snd end;
   1.335    in fold activate regs thy end;
   1.336  
   1.337 @@ -2046,27 +2069,26 @@
   1.338  
   1.339  (* activate instantiated facts in theory or context *)
   1.340  
   1.341 -structure Idtab =
   1.342 -  TableFun(type key = string * term list
   1.343 -    val ord = prod_ord string_ord (list_ord Term.fast_term_ord));
   1.344 -
   1.345 -fun gen_activate_facts_elemss mk_ctxt get_reg note note_interp attrib put_reg test_reg add_wit add_eqn
   1.346 -        prfx all_elemss propss eq_attns (exp, imp) thmss thy_ctxt =
   1.347 +fun gen_activate_facts_elemss mk_ctxt note note_interp attrib put_reg add_wit add_eqn
   1.348 +        prfx all_elemss pss propss eq_attns (exp, imp) thmss thy_ctxt =
   1.349    let
   1.350      val ctxt = mk_ctxt thy_ctxt;
   1.351 +    fun get_reg thy_ctxt = get_local_registration (mk_ctxt thy_ctxt);
   1.352 +    fun test_reg thy_ctxt = test_local_registration (mk_ctxt thy_ctxt);
   1.353 +
   1.354      val (all_propss, eq_props) = chop (length all_elemss) propss;
   1.355      val (all_thmss, eq_thms) = chop (length all_elemss) thmss;
   1.356  
   1.357      (* Filter out fragments already registered. *)
   1.358  
   1.359      val (new_elemss, xs) = split_list (filter_out (fn (((id, _), _), _) =>
   1.360 -          test_reg thy_ctxt id) (all_elemss ~~ (all_propss ~~ all_thmss)));
   1.361 -    val (new_propss, new_thmss) = split_list xs;
   1.362 +          test_reg thy_ctxt id) (all_elemss ~~ (pss ~~ (all_propss ~~ all_thmss))));
   1.363 +    val (new_pss, ys) = split_list xs;
   1.364 +    val (new_propss, new_thmss) = split_list ys;
   1.365  
   1.366      val thy_ctxt' = thy_ctxt
   1.367        (* add registrations *)
   1.368 -(*      |> fold (fn ((id, _), _) => put_reg id prfx (exp, imp)) new_elemss *)
   1.369 -      |> fold (fn (id, _) => put_reg id prfx (exp, imp)) new_propss
   1.370 +      |> fold (fn (((id, _), _), ps) => put_reg id (prfx, param_prefix ps) (exp, imp)) (new_elemss ~~ new_pss)
   1.371        (* add witnesses of Assumed elements (only those generate proof obligations) *)
   1.372        |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst new_propss ~~ new_thmss)
   1.373        (* add equations *)
   1.374 @@ -2078,66 +2100,64 @@
   1.375            (fn ((id, Assumed _), _) => Option.map #2 (get_reg thy_ctxt' imp id)
   1.376              | ((_, Derived _), _) => NONE) all_elemss);
   1.377  
   1.378 -    fun activate_elem eqns loc (fully_qualified, prfx) (Notes (kind, facts)) thy_ctxt =
   1.379 -        let
   1.380 -          val ctxt = mk_ctxt thy_ctxt;
   1.381 -          val facts' = interpret_args (ProofContext.theory_of ctxt) prfx
   1.382 -              (Symtab.empty, Symtab.empty) prems eqns exp (attrib thy_ctxt) facts;
   1.383 -        in snd (note_interp kind loc (fully_qualified, prfx) facts' thy_ctxt) end
   1.384 -      | activate_elem _ _ _ _ thy_ctxt = thy_ctxt;
   1.385 -
   1.386 -    fun activate_elems all_eqns ((id, _), elems) thy_ctxt =
   1.387 -      let
   1.388 -        val (prfx, _, _) = case get_reg thy_ctxt imp id
   1.389 -         of SOME x => x
   1.390 -          | NONE => sys_error ("Unknown registration of " ^ quote (fst id)
   1.391 -              ^ " while activating facts.");
   1.392 -      in fold (activate_elem (the (Idtab.lookup all_eqns id)) (fst id) prfx) elems thy_ctxt end;
   1.393 -
   1.394      val thy_ctxt'' = thy_ctxt'
   1.395        (* add witnesses of Derived elements *)
   1.396        |> fold (fn (id, thms) => fold (add_wit id o Element.morph_witness (Element.satisfy_morphism prems)) thms)
   1.397           (map_filter (fn ((_, Assumed _), _) => NONE
   1.398              | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
   1.399  
   1.400 -    (* Accumulate equations *)
   1.401 -    val all_eqns =
   1.402 -      fold_map (join_eqns (get_reg thy_ctxt'' imp) fst ctxt) all_propss Termtab.empty
   1.403 -      |> fst
   1.404 -      |> map (apsnd (map snd o Termtab.dest))
   1.405 -      |> (fn xs => fold Idtab.update xs Idtab.empty)
   1.406 -      (* Idtab.make wouldn't work here: can have conflicting duplicates,
   1.407 -         because instantiation may equate ids and equations are accumulated! *)
   1.408 +    fun activate_elem inst loc prfx pprfx (Notes (kind, facts)) thy_ctxt =
   1.409 +        let
   1.410 +          val ctxt = mk_ctxt thy_ctxt;
   1.411 +          val facts' = facts |>
   1.412 +              interpret_args (ProofContext.theory_of ctxt) inst exp (attrib thy_ctxt) |>
   1.413 +              add_param_prefixss pprfx;
   1.414 +        in snd (note_interp kind loc prfx facts' thy_ctxt) end
   1.415 +      | activate_elem _ _ _ _ _ thy_ctxt = thy_ctxt;
   1.416 +
   1.417 +    fun activate_elems ((((loc, ext_ts), _), _), ps) thy_ctxt =
   1.418 +      let
   1.419 +        val ctxt = mk_ctxt thy_ctxt;
   1.420 +        val thy = ProofContext.theory_of ctxt;
   1.421 +        val {params, elems, ...} = the_locale thy loc;
   1.422 +        val parms = map fst params;
   1.423 +        val pprfx = param_prefix ps;
   1.424 +        val ids = flatten (ProofContext.init thy, intern_expr thy)
   1.425 +          (([], Symtab.empty), Expr (Locale loc)) |> fst |> fst;
   1.426 +        val (insts, prems, eqns) = collect_witnesses ctxt imp parms ids ext_ts;
   1.427 +        val inst = inst_morph thy (snd prfx) pprfx insts prems eqns;
   1.428 +      in
   1.429 +        fold (activate_elem inst loc prfx pprfx) (map fst elems) thy_ctxt
   1.430 +      end;
   1.431  
   1.432    in
   1.433      thy_ctxt''
   1.434 -    (* add equations *)
   1.435 +    (* add equations as lemmas to context *)
   1.436      |> fold (fn (attns, thms) =>
   1.437           fold (fn (attn, thm) => note "lemma"
   1.438             [(apsnd (map (attrib thy_ctxt'')) attn,
   1.439               [([Element.conclude_witness thm], [])])] #> snd)
   1.440             (attns ~~ thms)) (unflat eq_thms eq_attns ~~ eq_thms)
   1.441 -    (* add facts *)
   1.442 -    |> fold (activate_elems all_eqns) new_elemss
   1.443 +    (* add interpreted facts *)
   1.444 +    |> fold activate_elems (new_elemss ~~ new_pss)
   1.445    end;
   1.446  
   1.447  fun global_activate_facts_elemss x = gen_activate_facts_elemss
   1.448        ProofContext.init
   1.449 -      get_global_registration
   1.450        PureThy.note_thmss
   1.451        global_note_prefix_i
   1.452        Attrib.attribute_i
   1.453 -      put_global_registration test_global_registration add_global_witness add_global_equation
   1.454 +      put_global_registration
   1.455 +      add_global_witness
   1.456 +      add_global_equation
   1.457        x;
   1.458  
   1.459  fun local_activate_facts_elemss x = gen_activate_facts_elemss
   1.460        I
   1.461 -      get_local_registration
   1.462        ProofContext.note_thmss_i
   1.463        local_note_prefix_i
   1.464        (Attrib.attribute_i o ProofContext.theory_of)
   1.465        put_local_registration
   1.466 -      test_local_registration
   1.467        add_local_witness
   1.468        add_local_equation
   1.469        x;
   1.470 @@ -2264,7 +2284,7 @@
   1.471  
   1.472      val propss = map extract_asms_elems inst_elemss @ eqn_elems;
   1.473  
   1.474 -  in (propss, activate prfx inst_elemss propss eq_attns morphs) end;
   1.475 +  in (propss, activate prfx inst_elemss (map (snd o fst) ids) propss eq_attns morphs) end;
   1.476  
   1.477  fun gen_prep_global_registration mk_ctxt = gen_prep_registration ProofContext.init
   1.478    test_global_registration
   1.479 @@ -2323,11 +2343,11 @@
   1.480                  |> fold (add_witness_in_locale target id) thms
   1.481            | activate_id _ thy = thy;
   1.482  
   1.483 -        fun activate_reg (vts, ((fully_qualified, prfx), (exp, imp), _, _)) thy =
   1.484 +        fun activate_reg (ext_ts, (((fully_qualified, prfx), pprfx), (exp, imp), _, _)) thy =
   1.485            let
   1.486 -            val (insts, wits, _) = collect_global_witnesses thy imp fixed target_ids vts;
   1.487 +            val (insts, wits, _) = collect_witnesses (ProofContext.init thy) imp fixed target_ids ext_ts;
   1.488              fun inst_parms ps = map
   1.489 -                  (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps;
   1.490 +                  (the o AList.lookup (op =) (map #1 fixed ~~ ext_ts)) ps;
   1.491              val disch = Element.satisfy_thm wits;
   1.492              val new_elemss = filter (fn (((name, ps), _), _) =>
   1.493                  not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
   1.494 @@ -2338,7 +2358,7 @@
   1.495                  if test_global_registration thy (name, ps')
   1.496                  then thy
   1.497                  else thy
   1.498 -                  |> put_global_registration (name, ps') (fully_qualified, prfx) (exp, imp)
   1.499 +                  |> put_global_registration (name, ps') ((fully_qualified, prfx), param_prefix ps) (exp, imp)
   1.500                    |> fold (fn witn => fn thy => add_global_witness (name, ps')
   1.501                       (Element.morph_witness (Element.inst_morphism thy insts) witn) thy) thms
   1.502                end;
   1.503 @@ -2350,7 +2370,7 @@
   1.504                  if test_global_registration thy (name, ps')
   1.505                  then thy
   1.506                  else thy
   1.507 -                  |> put_global_registration (name, ps') (fully_qualified, prfx) (exp, imp)
   1.508 +                  |> put_global_registration (name, ps') ((fully_qualified, prfx), param_prefix ps) (exp, imp)
   1.509                    |> fold (fn witn => fn thy => add_global_witness (name, ps')
   1.510                         (witn |> Element.map_witness (fn (t, th) =>  (* FIXME *)
   1.511                         (Element.inst_term insts t,
   1.512 @@ -2361,6 +2381,7 @@
   1.513                  let
   1.514                    val att_morphism =
   1.515                      Morphism.name_morphism (Name.qualified prfx) $>
   1.516 +(* FIXME? treatment of parameter prefix *)
   1.517                      Morphism.thm_morphism satisfy $>
   1.518                      Element.inst_morphism thy insts $>
   1.519                      Morphism.thm_morphism disch;