src/Pure/Isar/locale.ML

       (term * term list) list list
   val cert_context_statement: string option -> Element.context_i element list ->
     (term * term list) list list -> Proof.context ->
     string option * (cterm list * Proof.context) * (cterm list * Proof.context) *
       (term * term list) list list
+  val read_expr: expr -> Element.context list -> Proof.context ->
+    Element.context_i list * Proof.context
+  val cert_expr: expr -> Element.context_i list -> Proof.context ->
+    Element.context_i list * Proof.context
 
   (* Diagnostic functions *)
   val print_locales: theory -> unit
   val print_locale: theory -> bool -> expr -> Element.context list -> unit
   val print_global_registrations: bool -> string -> theory -> unit

 end;
 
 structure Locale: LOCALE =
 struct
 
+
 (** locale elements and expressions **)
 
 datatype ctxt = datatype Element.ctxt;
 
 datatype expr =

   Elem of 'a | Expr of expr;
 
 fun map_elem f (Elem e) = Elem (f e)
   | map_elem _ (Expr e) = Expr e;
 
-type witness = term * thm;  (*hypothesis as fact*)
 type locale =
- {predicate: cterm list * witness list,
+ {predicate: cterm list * Element.witness list,
     (* CB: For locales with "(open)" this entry is ([], []).
        For new-style locales, which declare predicates, if the locale declares
        no predicates, this is also ([], []).
        If the locale declares predicates, the record field is
        ([statement], axioms), where statement is the locale predicate applied

   import: expr,                                                     (*dynamic import*)
   elems: (Element.context_i * stamp) list,                          (*static content*)
   params: ((string * typ) * mixfix) list,                           (*all params*)
   lparams: string list,                                             (*local parmas*)
   term_syntax: ((Proof.context -> Proof.context) * stamp) list, (* FIXME depend on morphism *)
-  regs: ((string * string list) * (term * thm) list) list}
-    (* Registrations: indentifiers and witness theorems of locales interpreted
-       in the locale.
-    *)
+  regs: ((string * string list) * Element.witness list) list}
+    (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
 
 
 (* CB: an internal (Int) locale element was either imported or included,
    an external (Ext) element appears directly in the locale text. *)
 

 structure Registrations :
   sig
     type T
     val empty: T
     val join: T * T -> T
-    val dest: T -> (term list * ((string * Attrib.src list) * witness list)) list
+    val dest: T -> (term list * ((string * Attrib.src list) * Element.witness list)) list
     val lookup: theory -> T * term list ->
-      ((string * Attrib.src list) * witness list) option
+      ((string * Attrib.src list) * Element.witness list) option
     val insert: theory -> term list * (string * Attrib.src list) -> T ->
-      T * (term list * ((string * Attrib.src list) * witness list)) list
-    val add_witness: term list -> witness -> T -> T
+      T * (term list * ((string * Attrib.src list) * Element.witness list)) list
+    val add_witness: term list -> Element.witness -> T -> T
   end =
 struct
   (* a registration consists of theorems instantiating locale assumptions
      and prefix and attributes, indexed by parameter instantiation *)
-  type T = ((string * Attrib.src list) * witness list) Termtab.table;
+  type T = ((string * Attrib.src list) * Element.witness list) Termtab.table;
 
   val empty = Termtab.empty;
 
   (* term list represented as single term, for simultaneous matching *)
   fun termify ts =

   (* registrations that subsume t *)
   fun subsumers thy t regs =
     filter (fn (t', _) => Pattern.matches thy (t', t)) (Termtab.dest regs);
 
   (* look up registration, pick one that subsumes the query *)
-  fun lookup sign (regs, ts) =
+  fun lookup thy (regs, ts) =
     let
       val t = termify ts;
-      val subs = subsumers sign t regs;
+      val subs = subsumers thy t regs;
     in (case subs of
         [] => NONE
       | ((t', (attn, thms)) :: _) => let
-            val (tinst, inst) = Pattern.match sign (t', t) (Vartab.empty, Vartab.empty);
+            val (tinst, inst) = Pattern.match thy (t', t) (Vartab.empty, Vartab.empty);
             (* thms contain Frees, not Vars *)
             val tinst' = tinst |> Vartab.dest
                  |> map (fn ((x, 0), (_, T)) => (x, Type.unvarifyT T))
                  |> Symtab.make;
             val inst' = inst |> Vartab.dest
                  |> map (fn ((x, 0), (_, t)) => (x, Logic.unvarify t))
                  |> Symtab.make;
           in
-            SOME (attn, map (fn (t, th) =>
-             (Element.inst_term (tinst', inst') t,
-              Element.inst_thm sign (tinst', inst') th)) thms)
+            SOME (attn, map (Element.inst_witness thy (tinst', inst')) thms)
           end)
     end;
 
   (* add registration if not subsumed by ones already present,
      additionally returns registrations that are strictly subsumed *)

     val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
     fun prt_inst ts =
         Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts));
     fun prt_attn (prfx, atts) =
         Pretty.breaks (Pretty.str prfx :: Args.pretty_attribs ctxt atts);
-    fun prt_thm (_, th) = Pretty.quote (ProofContext.pretty_thm ctxt th);
-    fun prt_thms thms =
-        Pretty.enclose "[" "]" (Pretty.breaks (map prt_thm thms));
-    fun prt_reg (ts, (("", []), thms)) =
+    fun prt_witns witns = Pretty.enclose "[" "]"
+      (Pretty.breaks (map (prt_term o Element.witness_prop) witns));
+    fun prt_reg (ts, (("", []), witns)) =
         if show_wits
-          then Pretty.block [prt_inst ts, Pretty.fbrk, prt_thms thms]
+          then Pretty.block [prt_inst ts, Pretty.fbrk, prt_witns witns]
           else prt_inst ts
-      | prt_reg (ts, (attn, thms)) =
+      | prt_reg (ts, (attn, witns)) =
         if show_wits
           then Pretty.block ((prt_attn attn @
             [Pretty.str ":", Pretty.brk 1, prt_inst ts, Pretty.fbrk,
-              prt_thms thms]))
+              prt_witns witns]))
           else Pretty.block ((prt_attn attn @
             [Pretty.str ":", Pretty.brk 1, prt_inst ts]));
 
     val loc_int = intern thy loc;
     val regs = get_regs thy_ctxt;

 
 fun err_in_locale' ctxt msg ids' = err_in_locale ctxt msg (map fst ids');
 
 
 
-(** witnesses -- protected facts **)
-
-fun assume_protected thy t =
-  (t, Goal.protect (Thm.assume (Thm.cterm_of thy t)));
-
-fun prove_protected thy t tac =
-  (t, Goal.prove thy [] [] (Logic.protect t) (fn _ =>
-    Tactic.rtac Drule.protectI 1 THEN tac));
-
-val conclude_protected = Goal.conclude #> Goal.norm_hhf;
-
-fun satisfy_protected pths thm =
-  let
-    fun satisfy chyp =
-      (case find_first (fn (t, _) => Thm.term_of chyp aconv t) pths of
-        NONE => I
-      | SOME (_, th) => Drule.implies_intr_protected [chyp] #> Goal.comp_hhf th);
-  in fold satisfy (#hyps (Thm.crep_thm thm)) thm end;
-
-
-
 (** structured contexts: rename + merge + implicit type instantiation **)
 
 (* parameter types *)
 
 fun frozen_tvars ctxt Ts =

 
 
 (* Distinction of assumed vs. derived identifiers.
    The former may have axioms relating assumptions of the context to
    assumptions of the specification fragment (for locales with
-   predicates).  The latter have witness theorems relating assumptions of the
+   predicates).  The latter have witnesses relating assumptions of the
    specification fragment to assumptions of other (assumed) specification
    fragments. *)
 
 datatype 'a mode = Assumed of 'a | Derived of 'a;
 

       let
         val thy = ProofContext.theory_of ctxt;
         val envs = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss);
         fun inst ((((name, ps), mode), elems), env) =
           (((name, map (apsnd (Option.map (Element.instT_type env))) ps),
-              map_mode (map (fn (t, th) =>
-                (Element.instT_term env t, Element.instT_thm thy env th))) mode),
+              map_mode (map (Element.instT_witness thy env)) mode),
             map (Element.instT_ctxt thy env) elems);
       in map inst (elemss ~~ envs) end;
 
 (* like unify_elemss, but does not touch mode, additional
    parameter c_parms for enforcing further constraints (eg. syntax) *)

     fun rename_parms top ren ((name, ps), (parms, mode)) =
       let val ps' = map (Element.rename ren) ps in
         (case duplicates (op =) ps' of
           [] => ((name, ps'),
                  if top then (map (Element.rename ren) parms,
-                   map_mode (map (fn (t, th) =>
-                     (Element.rename_term ren t, Element.rename_thm ren th))) mode)
+                   map_mode (map (Element.rename_witness ren)) mode)
                  else (parms, mode))
         | dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')])
       end;
 
-    (* add registrations of (name, ps), recursively;
-       adjust hyps of witness theorems *)
+    (* add registrations of (name, ps), recursively; adjust hyps of witnesses *)
 
     fun add_regs (name, ps) (ths, ids) =
         let
           val {params, regs, ...} = the_locale thy name;
           val ps' = map #1 params;

               ((name, map (Element.rename ren) ps), ths)) regs;
           val new_regs = gen_rems (eq_fst (op =)) (regs', ids);
           val new_ids = map fst new_regs;
           val new_idTs = map (apsnd (map (fn p => (p, (the o AList.lookup (op =) ps) p)))) new_ids;
 
-          val new_ths = new_regs |> map (fn (_, ths') => ths' |> map (fn (t, th) =>
-           (t |> Element.instT_term env |> Element.rename_term ren,
-            th |> Element.instT_thm thy env |> Element.rename_thm ren |> satisfy_protected ths)));
+          val new_ths = new_regs |> map (#2 #> map
+            (Element.instT_witness thy env #>
+              Element.rename_witness ren #>
+              Element.satisfy_witness ths));
           val new_ids' = map (fn (id, ths) =>
               (id, ([], Derived ths))) (new_ids ~~ new_ths);
         in
           fold add_regs new_idTs (ths @ flat new_ths, ids @ new_ids')
         end;

          val [env] = unify_parms ctxt all_params [ps];
          val t' = Element.instT_term env t;
          val th' = Element.instT_thm thy env th;
        in (t', th') end;
     val final_elemss = map (fn ((id, mode), elems) =>
-         ((id, map_mode (map inst_th) mode), elems)) elemss';
+         ((id, map_mode (map (Element.map_witness inst_th)) mode), elems)) elemss';
 
   in ((prev_idents @ idents, syntax), final_elemss) end;
 
 end;
 

 (* activate elements *)
 
 local
 
 fun axioms_export axs _ hyps =
-  satisfy_protected axs
+  Element.satisfy_thm axs
   #> Drule.implies_intr_list (Library.drop (length axs, hyps))
   #> Seq.single;
 
 
 (* NB: derived ids contain only facts at this stage *)

           else let
               val ps' = map (fn (n, SOME T) => Free (n, T)) ps;
               val ctxt'' = put_local_registration (name, ps') ("", []) ctxt'
             in case mode of
                 Assumed axs =>
-                  fold (add_local_witness (name, ps') o assume_protected thy o #1) axs ctxt''
+                  fold (add_local_witness (name, ps') o
+                    Element.assume_witness thy o Element.witness_prop) axs ctxt''
               | Derived ths => fold (add_local_witness (name, ps')) ths ctxt''
             end
   in (ProofContext.restore_naming ctxt ctxt'', res) end;
 
 fun activate_elemss prep_facts =

 
 
 (* for finish_elems (Int),
    remove redundant elements of derived identifiers,
    turn assumptions and definitions into facts,
-   adjust hypotheses of facts using witness theorems *)
+   adjust hypotheses of facts using witnesses *)
 
 fun finish_derived _ _ (Assumed _) (Fixes fixes) = SOME (Fixes fixes)
   | finish_derived _ _ (Assumed _) (Constrains csts) = SOME (Constrains csts)
   | finish_derived _ _ (Assumed _) (Assumes asms) = SOME (Assumes asms)
   | finish_derived _ _ (Assumed _) (Defines defs) = SOME (Defines defs)
 
   | finish_derived _ _ (Derived _) (Fixes _) = NONE
   | finish_derived _ _ (Derived _) (Constrains _) = NONE
   | finish_derived sign wits (Derived _) (Assumes asms) = asms
       |> map (apsnd (map (fn (a, _) => ([Thm.assume (cterm_of sign a)], []))))
-      |> Notes |> Element.map_ctxt_values I I (satisfy_protected wits) |> SOME
+      |> Notes |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
   | finish_derived sign wits (Derived _) (Defines defs) = defs
       |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
-      |> Notes |> Element.map_ctxt_values I I (satisfy_protected wits) |> SOME
+      |> Notes |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME
 
   | finish_derived _ wits _ (Notes facts) = (Notes facts)
-      |> Element.map_ctxt_values I I (satisfy_protected wits) |> SOME;
+      |> Element.map_ctxt_values I I (Element.satisfy_thm wits) |> SOME;
 
 (* CB: for finish_elems (Ext) *)
 
 fun closeup _ false elem = elem
   | closeup ctxt true elem =

 fun cert_facts x = prep_facts (K I) (K I) x;
 
 end;
 
 
-(* Get the specification of a locale *)
-
-(* The global specification is made from the parameters and global
-   assumptions, the local specification from the parameters and the local
-   assumptions. *)
+(* specification of a locale *)
+
+(*The global specification is made from the parameters and global
+  assumptions, the local specification from the parameters and the
+  local assumptions.*)
 
 local
 
 fun gen_asms_of get thy name =
   let
     val ctxt = ProofContext.init thy;
     val (_, raw_elemss) = flatten (ctxt, I) (([], Symtab.empty), Expr (Locale name));
     val ((_, elemss, _), _) = read_elemss false ctxt [] raw_elemss [];
   in
     elemss |> get
-      |> map (fn (_, es) => map (fn Int e => e) es)
-      |> flat
-      |> map_filter (fn Assumes asms => SOME asms | _ => NONE)
-      |> flat
+      |> maps (fn (_, es) => map (fn Int e => e) es)
+      |> maps (fn Assumes asms => asms | _ => [])
       |> map (apsnd (map fst))
   end;
 
 in
 

   gen_asms_of (single o Library.last_elem) thy name;
 
 fun global_asms_of thy name =
   gen_asms_of I thy name;
 
-end (* local *)
+end;
 
 
 (* full context statements: import + elements + conclusion *)
 
 local

       activate_facts prep_facts (context, ps);
 
     val (ctxt, (elemss, _)) =
       activate_facts prep_facts (import_ctxt, qs);
     val stmt = distinct Term.aconv
-       (maps (fn ((_, Assumed axs), _) => maps (#hyps o Thm.rep_thm o #2) axs
+       (maps (fn ((_, Assumed axs), _) => maps Element.witness_hyps axs
                            | ((_, Derived _), _) => []) qs);
     val cstmt = map (cterm_of thy) stmt;
   in
     ((((import_ctxt, import_elemss), (ctxt, elemss, syn)), (parms, spec, defs)), (cstmt, concl))
   end;

           in (stmt, map fst ps, Locale name) end);
     val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), (elems_stmt, concl')) =
       prep_ctxt false fixed_params import elems concl ctxt;
   in (locale, (locale_stmt, locale_ctxt), (elems_stmt, elems_ctxt), concl') end;
 
+fun prep_expr prep import body ctxt =
+  let
+    val (((_, import_elemss), (ctxt', elemss, _)), _) = prep import body ctxt;
+    val all_elems = maps snd (import_elemss @ elemss);
+  in (all_elems, ctxt') end;
+
 in
 
 val read_ctxt = prep_context_statement intern_expr read_elemss read_facts;
 val cert_ctxt = prep_context_statement (K I) cert_elemss cert_facts;
 
 fun read_context import body ctxt = #1 (read_ctxt true [] import (map Elem body) [] ctxt);
 fun cert_context import body ctxt = #1 (cert_ctxt true [] import (map Elem body) [] ctxt);
 
+val read_expr = prep_expr read_context;
+val cert_expr = prep_expr cert_context;
+
 val read_context_statement = prep_statement intern read_ctxt;
 val cert_context_statement = prep_statement (K I) cert_ctxt;
 
 end;
 
 
 (* print locale *)
 
 fun print_locale thy show_facts import body =
   let
-    val (((_, import_elemss), (ctxt, elemss, _)), _) =
-      read_context import body (ProofContext.init thy);
+    val (all_elems, ctxt) = read_expr import body (ProofContext.init thy);
     val prt_elem = Element.pretty_ctxt ctxt;
-    val all_elems = maps #2 (import_elemss @ elemss);
   in
     Pretty.big_list "locale elements:" (all_elems
       |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
       |> map (Pretty.chunks o prt_elem))
     |> Pretty.writeln

 
 fun local_note_prefix_i prfx args ctxt =
   ctxt
   |> ProofContext.qualified_names
   |> ProofContext.sticky_prefix prfx
-  |> ProofContext.note_thmss_i args |> swap
-  |>> ProofContext.restore_naming ctxt;
-
-
-(* collect witness theorems for global registration;
+  |> ProofContext.note_thmss_i args
+  ||> ProofContext.restore_naming ctxt;
+
+
+(* collect witnesses for global registration;
    requires parameters and flattened list of (assumed!) identifiers
    instead of recomputing it from the target *)
 
 fun collect_global_witnesses thy parms ids vts = let
     val ts = map Logic.unvarify vts;

         val inst_atts =
           Args.map_values I (Element.instT_type (#1 insts))
             (Element.inst_term insts) (Element.inst_thm thy insts);
         val args' = args |> map (fn ((n, atts), [(ths, [])]) =>
             ((n, map (Attrib.attribute_i thy) (map inst_atts atts @ atts2)),
-             [(map (Drule.standard o satisfy_protected prems o
+             [(map (Drule.standard o Element.satisfy_thm prems o
             Element.inst_thm thy insts) ths, [])]));
       in global_note_prefix_i kind prfx args' thy |> snd end;
   in fold activate regs thy end;
 
 

     val conjuncts =
       (Drule.equal_elim_rule2 OF [body_eq,
         Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))])
       |> Conjunction.elim_precise [length ts] |> hd;
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
-      prove_protected defs_thy t
+      Element.prove_witness defs_thy t
        (Tactic.rewrite_goals_tac defs THEN
         Tactic.compose_tac (false, ax, 0) 1));
   in ((statement, intro, axioms), defs_thy) end;
 
 fun assumes_to_notes (Assumes asms) axms =

 
 fun change_elemss axioms elemss =
   let
     fun change (id as ("", _), es)=
           fold_map assumes_to_notes
-            (map (Element.map_ctxt_values I I (satisfy_protected axioms)) es)
+            (map (Element.map_ctxt_values I I (Element.satisfy_thm axioms)) es)
           #-> (fn es' => pair (id, es'))
       | change e = pair e;
   in
-    fst (fold_map change elemss (map (conclude_protected o snd) axioms))
+    fst (fold_map change elemss (map Element.conclude_witness axioms))
   end;
 
 in
 
 (* CB: main predicate definition function *)

           val cstatement = Thm.cterm_of def_thy statement;
         in
           def_thy
           |> PureThy.note_thmss_qualified "" bname
                [((introN, []), [([intro], [])]),
-                ((axiomsN, []), [(map (Drule.standard o conclude_protected o #2) axioms, [])])]
+                ((axiomsN, []), [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
           |> snd
           |> pair ([cstatement], axioms)
         end;
   in ((elemss', predicate), thy'') end;
 

       theorem_in_locale kind NONE (K (K I)) loc a elems concl;
 
 end;
 
 
+
 (** Interpretation commands **)
 
 local
 
 (* extract proof obligations (assms and defs) from elements *)
 
-fun extract_asms_elem (Fixes _) ts = ts
-  | extract_asms_elem (Constrains _) ts = ts
-  | extract_asms_elem (Assumes asms) ts =
-      ts @ maps (fn (_, ams) => map (fn (t, _) => t) ams) asms
-  | extract_asms_elem (Defines defs) ts =
-      ts @ map (fn (_, (def, _)) => def) defs
-  | extract_asms_elem (Notes _) ts = ts;
-
-fun extract_asms_elems ((id, Assumed _), elems) =
-      (id, fold extract_asms_elem elems [])
+fun extract_asms_elems ((id, Assumed _), elems) = (id, maps Element.prems_of elems)
   | extract_asms_elems ((id, Derived _), _) = (id, []);
 
-fun extract_asms_elemss elemss = map extract_asms_elems elemss;
 
 (* activate instantiated facts in theory or context *)
 
 fun gen_activate_facts_elemss get_reg note attrib std put_reg add_wit
         attn all_elemss new_elemss propss thmss thy_ctxt =

               |> Attrib.map_facts (attrib thy_ctxt o Args.map_values I I I disch)
               (* insert interpretation attributes *)
               |> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts)))
               (* discharge hyps *)
               |> map (apsnd (map (apfst (map disch))));
-          in fst (note prfx facts' thy_ctxt) end
+          in snd (note prfx facts' thy_ctxt) end
         | activate_elem _ _ _ thy_ctxt = thy_ctxt;
 
       fun activate_elems disch ((id, _), elems) thy_ctxt =
           let
             val ((prfx, atts2), _) = the (get_reg thy_ctxt id)

 
       val thy_ctxt' = thy_ctxt
         (* add registrations *)
         |> fold (fn ((id, _), _) => put_reg id attn) new_elemss
         (* add witnesses of Assumed elements *)
-        |> fold (fn (id, thms) => fold (add_wit id) thms)
-           (map fst propss ~~ thmss);
+        |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst propss ~~ thmss);
 
       val prems = flat (map_filter
             (fn ((id, Assumed _), _) => Option.map snd (get_reg thy_ctxt' id)
               | ((_, Derived _), _) => NONE) all_elemss);
-      val disch = satisfy_protected prems;
-      val disch' = std o disch;  (* FIXME *)
-
       val thy_ctxt'' = thy_ctxt'
         (* add witnesses of Derived elements *)
-        |> fold (fn (id, thms) => fold (add_wit id o apsnd disch) thms)
+        |> fold (fn (id, thms) => fold (add_wit id o Element.satisfy_witness prems) thms)
            (map_filter (fn ((_, Assumed _), _) => NONE
               | ((id, Derived thms), _) => SOME (id, thms)) all_elemss)
+
+      val disch' = std o Element.satisfy_thm prems;  (* FIXME *)
     in
       thy_ctxt''
         (* add facts to theory or context *)
         |> fold (activate_elems disch') new_elemss
     end;
 
 fun global_activate_facts_elemss x = gen_activate_facts_elemss
       (fn thy => fn (name, ps) =>
         get_global_registration thy (name, map Logic.varify ps))
-      (swap ooo global_note_prefix_i "")
+      (global_note_prefix_i "")
       Attrib.attribute_i Drule.standard
       (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
-      (fn (n, ps) => fn (t, th) =>
-         add_global_witness (n, map Logic.varify ps)
-         (Logic.unvarify t, Drule.freeze_all th)) x;
+      (fn (n, ps) => add_global_witness (n, map Logic.varify ps) o
+        Element.map_witness (fn (t, th) => (Logic.unvarify t, Drule.freeze_all th))
+        (* FIXME *)) x;
 
 fun local_activate_facts_elemss x = gen_activate_facts_elemss
       get_local_registration
       local_note_prefix_i
       (Attrib.attribute_i o ProofContext.theory_of) I

           ((n, map (fn p => Free (p, (the o AList.lookup (op =) parms) p)) ps), mode)) ids;
     (* instantiate ids and elements *)
     val inst_elemss = (ids' ~~ all_elemss) |> map (fn (((n, ps), _), ((_, mode), elems)) =>
       ((n, map (Element.inst_term insts) ps),
         map (fn Int e => Element.inst_ctxt thy insts e) elems)
-      |> apfst (fn id => (id, map_mode (map (fn (t, th) =>
-          (Element.inst_term insts t, Element.inst_thm thy insts th))) mode)));
+      |> apfst (fn id => (id, map_mode (map (Element.inst_witness thy insts)) mode)));
 
     (* remove fragments already registered with theory or context *)
     val new_inst_elemss = filter (fn ((id, _), _) =>
           not (test_reg thy_ctxt id)) inst_elemss;
     val new_ids = map #1 new_inst_elemss;
 
-    val propss = extract_asms_elemss new_inst_elemss;
+    val propss = map extract_asms_elems new_inst_elemss;
 
     val bind_attrib = Attrib.crude_closure ctxt o Args.assignable;
     val attn' = apsnd (map (bind_attrib o Attrib.intern_src thy)) attn;
 
   in (propss, activate attn' inst_elemss new_inst_elemss propss) end;

     (* remove Int markers *)
     val elemss' = map (fn (_, es) =>
         map (fn Int e => e) es) elemss
     (* extract assumptions and defs *)
     val ids_elemss = ids' ~~ elemss';
-    val propss = extract_asms_elemss ids_elemss;
+    val propss = map extract_asms_elems ids_elemss;
 
     (** activation function:
         - add registrations to the target locale
         - add induced registrations for all global registrations of
           the target, unless already present

 
     val t_ids = map_filter
         (fn (id, (_, Assumed _)) => SOME id | _ => NONE) target_ids;
 
     fun activate thmss thy = let
-        val satisfy = satisfy_protected (flat thmss);
+        val satisfy = Element.satisfy_thm (flat thmss);
         val ids_elemss_thmss = ids_elemss ~~ thmss;
         val regs = get_global_registrations thy target;
 
         fun activate_id (((id, Assumed _), _), thms) thy =
             thy |> put_registration_in_locale target id

 
         fun activate_reg (vts, ((prfx, atts2), _)) thy = let
             val (insts, wits) = collect_global_witnesses thy fixed t_ids vts;
             fun inst_parms ps = map
                   (the o AList.lookup (op =) (map #1 fixed ~~ vts)) ps;
-            val disch = satisfy_protected wits;
+            val disch = Element.satisfy_thm wits;
             val new_elemss = filter (fn (((name, ps), _), _) =>
                 not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
             fun activate_assumed_id (((_, Derived _), _), _) thy = thy
               | activate_assumed_id ((((name, ps), Assumed _), _), thms) thy = let
                 val ps' = inst_parms ps;
               in
                 if test_global_registration thy (name, ps')
                 then thy
                 else thy
                   |> put_global_registration (name, ps') (prfx, atts2)
-                  |> fold (fn (t, th) => fn thy => add_global_witness (name, ps')
-                     (Element.inst_term insts t, disch (Element.inst_thm thy insts th)) thy) thms
+                  |> fold (fn witn => fn thy => add_global_witness (name, ps')
+                     (Element.inst_witness thy insts witn) thy) thms
               end;
 
             fun activate_derived_id ((_, Assumed _), _) thy = thy
               | activate_derived_id (((name, ps), Derived ths), _) thy = let
                 val ps' = inst_parms ps;
               in
                 if test_global_registration thy (name, ps')
                 then thy
                 else thy
                   |> put_global_registration (name, ps') (prfx, atts2)
-                  |> fold (fn (t, th) => fn thy => add_global_witness (name, ps')
+                  |> fold (fn witn => fn thy => add_global_witness (name, ps')
+                       (witn |> Element.map_witness (fn (t, th) =>  (* FIXME *)
                        (Element.inst_term insts t,
-                        disch (Element.inst_thm thy insts (satisfy th))) thy) ths
+                        disch (Element.inst_thm thy insts (satisfy th))))) thy) ths
               end;
 
             fun activate_elem (Notes facts) thy =
                 let
                   val facts' = facts

       end;
 
   in (propss, activate) end;
 
 fun prep_propp propss = propss |> map (fn ((name, _), props) =>
-  (("", []), map (rpair [] o Logic.protect) props));
+  (("", []), map (rpair [] o Element.mark_witness) props));
 
 fun prep_result propps thmss =
-  ListPair.map (fn ((_, props), thms) => (props ~~ thms)) (propps, thmss);
-
-val refine_protected =
-  Proof.refine (Method.Basic (K (Method.RAW_METHOD
-    (K (ALLGOALS
-      (PRECISE_CONJUNCTS ~1 (ALLGOALS
-        (PRECISE_CONJUNCTS ~1 (ALLGOALS (Tactic.rtac Drule.protectI))))))))))
-  #> Seq.hd;
+  ListPair.map (fn ((_, props), thms) => map2 Element.make_witness props thms) (propps, thmss);
 
 fun goal_name thy kind target propss =
     kind ^ Proof.goal_names (Option.map (extern thy) target) ""
       (propss |> map (fn ((name, _), _) => extern thy name));
 

     val kind = goal_name thy "interpretation" NONE propss;
     val after_qed = activate o prep_result propss;
   in
     ProofContext.init thy
     |> Proof.theorem_i kind NONE after_qed NONE ("", []) (prep_propp propss)
-    |> refine_protected
+    |> Element.refine_witness
   end;
 
 fun interpretation_in_locale (raw_target, expr) thy =
   let
     val target = intern thy raw_target;

     val after_qed = K (activate o prep_result propss);
   in
     thy
     |> theorem_in_locale_no_target kind NONE after_qed target ("", []) []
       (Element.Shows (prep_propp propss))
-    |> refine_protected
+    |> Element.refine_witness
   end;
 
 fun interpret (prfx, atts) expr insts int state =
   let
     val _ = Proof.assert_forward_or_chain state;

       #> Seq.single;
   in
     state
     |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
       kind NONE after_qed (prep_propp propss)
-    |> refine_protected
+    |> Element.refine_witness
   end;
 
 end;
 
 end;