# HG changeset patch
# User wenzelm
# Date 1149537266 -7200
# Node ID dce2168b0ea480c34afebcb93194b1d8d55b0eb8
# Parent  5c77dfb74c7bc425cf76dba4534d4d4084ff1fb7
export read/cert_expr;
moved type witness to element.ML (abstract type);
tuned;

diff -r 5c77dfb74c7b -r dce2168b0ea4 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Jun 05 21:54:25 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Jun 05 21:54:26 2006 +0200
@@ -63,6 +63,10 @@
     (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
@@ -117,6 +121,7 @@
 structure Locale: LOCALE =
 struct
 
+
 (** locale elements and expressions **)
 
 datatype ctxt = datatype Element.ctxt;
@@ -134,9 +139,8 @@
 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 ([], []).
@@ -151,10 +155,8 @@
   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,
@@ -171,17 +173,17 @@
     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;
 
@@ -204,14 +206,14 @@
     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))
@@ -220,9 +222,7 @@
                  |> 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;
 
@@ -432,18 +432,17 @@
         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]));
 
@@ -491,27 +490,6 @@
 
 
 
-(** 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 *)
@@ -560,7 +538,7 @@
 (* 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. *)
 
@@ -628,8 +606,7 @@
         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;
 
@@ -686,14 +663,12 @@
         (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
@@ -710,9 +685,10 @@
           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
@@ -823,7 +799,7 @@
          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;
 
@@ -835,7 +811,7 @@
 local
 
 fun axioms_export axs _ hyps =
-  satisfy_protected axs
+  Element.satisfy_thm axs
   #> Drule.implies_intr_list (Library.drop (length axs, hyps))
   #> Seq.single;
 
@@ -887,7 +863,8 @@
               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;
@@ -1103,7 +1080,7 @@
 (* 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)
@@ -1114,13 +1091,13 @@
   | 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) *)
 
@@ -1292,11 +1269,11 @@
 end;
 
 
-(* Get the specification of a locale *)
+(* 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. *)
+(*The global specification is made from the parameters and global
+  assumptions, the local specification from the parameters and the
+  local assumptions.*)
 
 local
 
@@ -1307,10 +1284,8 @@
     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;
 
@@ -1333,7 +1308,7 @@
 fun global_asms_of thy name =
   gen_asms_of I thy name;
 
-end (* local *)
+end;
 
 
 (* full context statements: import + elements + conclusion *)
@@ -1369,7 +1344,7 @@
     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
@@ -1390,6 +1365,12 @@
       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;
@@ -1398,6 +1379,9 @@
 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;
 
@@ -1408,10 +1392,8 @@
 
 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))
@@ -1436,11 +1418,11 @@
   ctxt
   |> ProofContext.qualified_names
   |> ProofContext.sticky_prefix prfx
-  |> ProofContext.note_thmss_i args |> swap
-  |>> ProofContext.restore_naming ctxt;
+  |> ProofContext.note_thmss_i args
+  ||> ProofContext.restore_naming ctxt;
 
 
-(* collect witness theorems for global registration;
+(* collect witnesses for global registration;
    requires parameters and flattened list of (assumed!) identifiers
    instead of recomputing it from the target *)
 
@@ -1482,7 +1464,7 @@
             (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;
@@ -1626,7 +1608,7 @@
         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;
@@ -1645,11 +1627,11 @@
   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
@@ -1685,7 +1667,7 @@
           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;
@@ -1853,25 +1835,16 @@
 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 *)
 
@@ -1887,7 +1860,7 @@
               |> 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 =
@@ -1903,20 +1876,18 @@
         (* 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 *)
@@ -1926,12 +1897,12 @@
 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
@@ -2013,15 +1984,14 @@
     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;
@@ -2063,7 +2033,7 @@
         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
@@ -2075,7 +2045,7 @@
         (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;
 
@@ -2088,7 +2058,7 @@
             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
@@ -2099,8 +2069,8 @@
                 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
@@ -2111,9 +2081,10 @@
                 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 =
@@ -2145,17 +2116,10 @@
   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) ""
@@ -2171,7 +2135,7 @@
   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 =
@@ -2184,7 +2148,7 @@
     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 =
@@ -2201,7 +2165,7 @@
     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;