# HG changeset patch
# User wenzelm
# Date 1131442995 -3600
# Node ID 1bb572e8cee91ef9892212893d0fda4f3a606562
# Parent  d5a876195499f9f4cb8fd9d4421bdef53cb1732f
avoid prove_plain, export_plain, simplified after_qed;
witness = term * thm, i.e. the original proposition with a protected fact
  (this achieves reliable discharge and allows facts to be slightly more general/normalized);
internal assume/prove/conclude/satisfy_protected handle witness pairs accordingly;
ObjectLogic.ensure_propT;

diff -r d5a876195499 -r 1bb572e8cee9 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Nov 08 10:43:13 2005 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Nov 08 10:43:15 2005 +0100
@@ -91,23 +91,21 @@
   val note_thmss_i: string -> string ->
     ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     theory -> (theory * ProofContext.context) * (bstring * thm list) list
-  val theorem: string -> Method.text option ->
-    (context * thm list -> thm list list -> theory -> theory) ->
+  val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
     string * Attrib.src list -> element elem_expr list ->
     ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
     theory -> Proof.state
-  val theorem_i: string -> Method.text option ->
-    (context * thm list -> thm list list -> theory -> theory) ->
+  val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) ->
     string * theory attribute list -> element_i elem_expr list ->
     ((string * theory attribute list) * (term * (term list * term list)) list) list ->
     theory -> Proof.state
   val theorem_in_locale: string -> Method.text option ->
-    ((context * context) * thm list -> thm list list -> theory -> theory) ->
+    (thm list list -> thm list list -> theory -> theory) ->
     xstring -> string * Attrib.src list -> element elem_expr list ->
     ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
     theory -> Proof.state
   val theorem_in_locale_i: string -> Method.text option ->
-    ((context * context) * thm list -> thm list list -> theory -> theory) ->
+    (thm list list -> thm list list -> theory -> theory) ->
     string -> string * Attrib.src list -> element_i elem_expr list ->
     ((string * Attrib.src list) * (term * (term list * term list)) list) list ->
     theory -> Proof.state
@@ -125,6 +123,7 @@
 structure Locale: LOCALE =
 struct
 
+
 (** locale elements and expressions **)
 
 type context = ProofContext.context;
@@ -149,8 +148,9 @@
 datatype 'a elem_expr =
   Elem of 'a | Expr of expr;
 
+type witness = term * thm;  (*hypothesis as fact*)
 type locale =
- {predicate: cterm list * thm list,
+ {predicate: cterm list * 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 ([], []).
@@ -164,7 +164,7 @@
   elems: (element_i * stamp) list,                    (*static content*)
   params: ((string * typ) * mixfix option) list * string list,
                                                       (*all/local params*)
-  regs: ((string * string list) * thm list) list}
+  regs: ((string * string list) * (term * thm) list) list}
     (* Registrations: indentifiers and witness theorems of locales interpreted
        in the locale.
     *)
@@ -277,17 +277,17 @@
     type T
     val empty: T
     val join: T * T -> T
-    val dest: T -> (term list * ((string * Attrib.src list) * thm list)) list
+    val dest: T -> (term list * ((string * Attrib.src list) * witness list)) list
     val lookup: theory -> T * term list ->
-      ((string * Attrib.src list) * thm list) option
+      ((string * Attrib.src list) * witness list) option
     val insert: theory -> term list * (string * Attrib.src list) -> T ->
-      T * (term list * ((string * Attrib.src list) * thm list)) list
-    val add_witness: term list -> thm -> T -> T
+      T * (term list * ((string * Attrib.src list) * witness list)) list
+    val add_witness: term list -> 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) * thm list) Termtab.table;
+  type T = ((string * Attrib.src list) * witness list) Termtab.table;
 
   val empty = Termtab.empty;
 
@@ -326,7 +326,8 @@
                  |> map (fn ((x, 0), (_, t)) => (x, Logic.unvarify t))
                  |> Symtab.make;
           in
-            SOME (attn, map (inst_tab_thm sign (inst', tinst')) thms)
+            SOME (attn, map (fn (t, th) =>
+              (inst_tab_term (inst', tinst') t, inst_tab_thm sign (inst', tinst') th)) thms)
           end)
     end;
 
@@ -499,14 +500,13 @@
 (* add witness theorem to registration in theory or context,
    ignored if registration not present *)
 
-fun gen_add_witness map_regs (name, ps) thm =
-  map_regs (Symtab.map_entry name (Registrations.add_witness ps thm));
-
-val add_global_witness =
-     gen_add_witness (fn f =>
-       GlobalLocalesData.map (fn (space, locs, regs) =>
-         (space, locs, f regs)));
-val add_local_witness = gen_add_witness LocalLocalesData.map;
+fun add_witness (name, ps) thm =
+  Symtab.map_entry name (Registrations.add_witness ps thm);
+
+fun add_global_witness id thm =
+  GlobalLocalesData.map (fn (space, locs, regs) => (space, locs, add_witness id thm regs));
+
+val add_local_witness = LocalLocalesData.map oo add_witness;
 
 fun add_witness_in_locale name id thm thy =
     let
@@ -547,7 +547,7 @@
         Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts));
     fun prt_attn (prfx, atts) =
         Pretty.breaks (Pretty.str prfx :: Args.pretty_attribs ctxt atts);
-    val prt_thm = Pretty.quote o ProofContext.pretty_thm ctxt;
+    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)) =
@@ -740,12 +740,33 @@
       ((n, map (inst_tab_term inst) ps), map (inst_tab_elem thy inst) elems);
 
 
+(* protected thms *)
+
+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 *)
 
 (* CB: frozen_tvars has the following type:
-  ProofContext.context -> Term.typ list -> (Term.indexname * (sort * Term.typ)) list *)
+  ProofContext.context -> typ list -> (indexname * (sort * typ)) list *)
 
 fun frozen_tvars ctxt Ts =
   let
@@ -801,6 +822,7 @@
 fun map_mode f (Assumed x) = Assumed (f x)
   | map_mode f (Derived x) = Derived (f x);
 
+
 (* flatten expressions *)
 
 local
@@ -853,7 +875,7 @@
       |> List.mapPartial (fn (a, S) =>
           let val T = Envir.norm_type unifier' (TVar ((a, i), S))
           in if T = TFree (a, S) then NONE else SOME ((a, S), T) end)
-  in map inst_parms idx_parmss end : ((string * Term.sort) * Term.typ) list list;
+  in map inst_parms idx_parmss end : ((string * sort) * typ) list list;
 
 in
 
@@ -864,7 +886,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 (inst_type env))) ps), 
-              map_mode (map (inst_thm ctxt env)) mode),
+              map_mode (map (fn (t, th) => (inst_term env t, inst_thm ctxt env th))) mode),
             map (inst_elem ctxt env) elems);
       in map inst (elemss ~~ envs) end;
 
@@ -922,7 +944,8 @@
         (case duplicates ps' of
           [] => ((name, ps'),
                  if top then (map (rename ren) parms,
-                   map_mode (map (rename_thm ren)) mode)
+                   map_mode (map (fn (t, th) =>
+                     (rename_term ren t, rename_thm ren th))) mode)
                  else (parms, mode))
         | dups => err_in_locale ctxt ("Duplicate parameters: " ^ commas_quote dups) [(name, ps')])
       end;
@@ -945,8 +968,9 @@
           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 = map (fn (_, ths') =>
-              map (Drule.satisfy_hyps ths o rename_thm ren o inst_thm ctxt env) ths') new_regs;
+          val new_ths = new_regs |> map (fn (_, ths') => ths' |> map (fn (t, th) =>
+           (t |> inst_term env |> rename_term ren,
+            th |> inst_thm ctxt env |> rename_thm ren |> satisfy_protected ths)));
           val new_ids' = map (fn (id, ths) =>
               (id, ([], Derived ths))) (new_ids ~~ new_ths);
         in
@@ -1052,12 +1076,13 @@
     val elemss' = map (fn (((name, _), (ps, mode)), elems) =>
          (((name, map (fn p => (p, AList.lookup (op =) all_params p)) ps), mode), elems))
          elemss;
-    fun inst_th th = let
+    fun inst_th (t, th) = let
          val {hyps, prop, ...} = Thm.rep_thm th;
          val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
          val [env] = unify_parms ctxt all_params [ps];
+         val t' = inst_term env t;
          val th' = inst_thm ctxt env th;
-       in th' end;
+       in (t', th') end;
     val final_elemss = map (fn ((id, mode), elems) =>
          ((id, map_mode (map inst_th) mode), elems)) elemss';
 
@@ -1070,12 +1095,10 @@
 
 local
 
-fun export_axioms axs _ hyps th =
-  th |> Drule.satisfy_hyps axs
-     (* CB: replace meta-hyps, using axs, by a single meta-hyp. *)
-  |> Drule.implies_intr_list (Library.drop (length axs, hyps))
-     (* CB: turn remaining hyps into assumptions. *)
-  |> Seq.single
+fun export_axioms axs _ hyps =
+  satisfy_protected axs
+  #> Drule.implies_intr_list (Library.drop (length axs, hyps))
+  #> Seq.single;
 
 
 (* NB: derived ids contain only facts at this stage *)
@@ -1114,6 +1137,7 @@
 
 fun activate_elems (((name, ps), mode), elems) ctxt =
   let
+    val thy = ProofContext.theory_of ctxt;
     val ((ctxt', _), res) =
         foldl_map (activate_elem (name = "")) ((ProofContext.qualified_names ctxt, mode), elems)
       handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)]
@@ -1122,11 +1146,9 @@
               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 (fn ax => fn ctxt =>
-                      add_local_witness (name, ps')
-                       (Thm.assume (Thm.cprop_of ax)) ctxt) axs ctxt''
-                 | Derived ths => fold (fn th => fn ctxt =>
-                     add_local_witness (name, ps') th ctxt) ths ctxt''
+                Assumed axs =>
+                  fold (add_local_witness (name, ps') o assume_protected thy o #1) axs ctxt''
+              | Derived ths => fold (add_local_witness (name, ps')) ths ctxt''
             end
   in (ProofContext.restore_naming ctxt ctxt'', res) end;
 
@@ -1366,9 +1388,6 @@
    turn assumptions and definitions into facts,
    adjust hypotheses of facts using witness theorems *)
 
-fun finish_derived _ wits _ (Notes facts) = (Notes facts)
-      |> map_values I I (Drule.satisfy_hyps wits) |> SOME;
-
 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)
@@ -1378,13 +1397,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 |> map_values I I (Drule.satisfy_hyps wits) |> SOME
+      |> Notes |> map_values I I (satisfy_protected wits) |> SOME
   | finish_derived sign wits (Derived _) (Defines defs) = defs
       |> map (apsnd (fn (d, _) => [([Thm.assume (cterm_of sign d)], [])]))
-      |> Notes |> map_values I I (Drule.satisfy_hyps wits) |> SOME
+      |> Notes |> map_values I I (satisfy_protected wits) |> SOME
 
   | finish_derived _ wits _ (Notes facts) = (Notes facts)
-      |> map_values I I (Drule.satisfy_hyps wits) |> SOME;
+      |> map_values I I (satisfy_protected wits) |> SOME;
 
 (* CB: for finish_elems (Ext) *)
 
@@ -1596,7 +1615,7 @@
       activate_facts prep_facts (import_ctxt, qs);
     val stmt = gen_distinct Term.aconv
        (List.concat (map (fn ((_, Assumed axs), _) =>
-         List.concat (map (#hyps o Thm.rep_thm) axs)
+         List.concat (map (#hyps o Thm.rep_thm o #2) axs)
                            | ((_, Derived _), _) => []) qs));
     val cstmt = map (cterm_of thy) stmt;
   in
@@ -1622,9 +1641,8 @@
 
 in
 
-(* CB: arguments are: x->import, y->body (elements), z->context *)
-fun read_context x y z = #1 (gen_context true [] x (map Elem y) [] z);
-fun cert_context x y z = #1 (gen_context_i true [] x (map Elem y) [] z);
+fun read_context import body ctxt = #1 (gen_context true [] import (map Elem body) [] ctxt);
+fun cert_context import body ctxt = #1 (gen_context_i true [] import (map Elem body) [] ctxt);
 
 val read_context_statement = gen_statement intern gen_context;
 val cert_context_statement = gen_statement (K I) gen_context_i;
@@ -1781,7 +1799,7 @@
             ((NameSpace.qualified prfx n,
               map (Attrib.global_attribute_i thy)
                   (inst_tab_atts thy (inst, tinst) atts @ atts2)),
-             [(map (Drule.standard o Drule.satisfy_hyps prems o
+             [(map (Drule.standard o satisfy_protected prems o
                 inst_tab_thm thy (inst, tinst)) ths, [])]))
           args;
       in global_note_accesses_i (Drule.kind kind) prfx args' thy |> fst end;
@@ -1896,7 +1914,7 @@
 
     val args = map Logic.mk_type extraTs @ map Free xs;
     val head = Term.list_comb (Const (name, predT), args);
-    val statement = ObjectLogic.assert_propT thy head;
+    val statement = ObjectLogic.ensure_propT thy head;
 
     val (defs_thy, [pred_def]) =
       thy
@@ -1917,27 +1935,22 @@
         Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))])
       |> Drule.conj_elim_precise (length ts);
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
-      Goal.prove_plain defs_thy [] [] t (fn _ =>
-        Tactic.rewrite_goals_tac defs THEN
+      prove_protected defs_thy t
+       (Tactic.rewrite_goals_tac defs THEN
         Tactic.compose_tac (false, ax, 0) 1));
   in (defs_thy, (statement, intro, axioms)) end;
 
-(* CB: modify the locale elements:
-   - assumes elements become notes elements,
-   - notes elements are lifted
-*)
-
-fun change_elem (axms, Assumes asms) =
+fun assumes_to_notes (axms, Assumes asms) =
       apsnd Notes ((axms, asms) |> foldl_map (fn (axs, (a, spec)) =>
-        let val (ps,qs) = splitAt(length spec, axs)
+        let val (ps, qs) = splitAt (length spec, axs)
         in (qs, (a, [(ps, [])])) end))
-  | change_elem e = e;
+  | assumes_to_notes e = e;
 
 (* CB: changes only "new" elems, these have identifier ("", _). *)
 
-fun change_elemss axioms elemss = (axioms, elemss) |> foldl_map
+fun change_elemss axioms elemss = (map (conclude_protected o #2) axioms, elemss) |> foldl_map
   (fn (axms, (id as ("", _), es)) =>
-    foldl_map change_elem (axms, map (map_values I I (Drule.satisfy_hyps axioms)) es)
+    foldl_map assumes_to_notes (axms, map (map_values I I (satisfy_protected axioms)) es)
     |> apsnd (pair id)
   | x => x) |> #2;
 
@@ -1954,7 +1967,7 @@
           val aname = if null ints then bname else bname ^ "_" ^ axiomsN;
           val (def_thy, (statement, intro, axioms)) =
             thy |> def_pred aname parms defs exts exts';
-          val elemss' = change_elemss (map (Drule.zero_var_indexes o Drule.gen_all) axioms) elemss @
+          val elemss' = change_elemss axioms elemss @
             [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])];
         in
           def_thy |> note_thmss_qualified "" aname
@@ -1971,7 +1984,7 @@
         in
           def_thy |> note_thmss_qualified "" bname
             [((introN, []), [([intro], [])]),
-             ((axiomsN, []), [(map Drule.standard axioms, [])])]
+             ((axiomsN, []), [(map (Drule.standard o conclude_protected o #2) axioms, [])])]
           |> #1 |> rpair ([cstatement], axioms)
         end;
   in (thy'', (elemss', predicate)) end;
@@ -2076,23 +2089,25 @@
     val thy_ctxt = ProofContext.init thy;
     val (_, (locale_view, elems_view), locale_ctxt, elems_ctxt, propp) =
       prep_stmt (SOME raw_locale) elems (map snd concl) thy_ctxt;
-    val elems_ctxt' = elems_ctxt |> ProofContext.add_view locale_ctxt elems_view;
-    val elems_ctxt'' = elems_ctxt' |> ProofContext.add_view thy_ctxt locale_view;
-    val locale_ctxt' = locale_ctxt |> ProofContext.add_view thy_ctxt locale_view;
+    val elems_ctxt' = elems_ctxt
+      |> ProofContext.add_view locale_ctxt elems_view
+      |> ProofContext.add_view thy_ctxt locale_view;
+    val locale_ctxt' = locale_ctxt
+      |> ProofContext.add_view thy_ctxt locale_view;
       
     val stmt = map (apsnd (K []) o fst) concl ~~ propp;
 
-    fun after_qed' (goal_ctxt, raw_results) results =
-      let val res = results |> (map o map)
-          (ProofContext.export elems_ctxt' locale_ctxt) in
-        curry (add_thmss kind locale ((names ~~ locale_attss) ~~ res)) locale_ctxt
-        #-> (fn res' =>
+    fun after_qed' results =
+      let val locale_results = results |> (map o map)
+          (ProofContext.export elems_ctxt' locale_ctxt') in
+        curry (add_thmss kind locale ((names ~~ locale_attss) ~~ locale_results)) locale_ctxt
+        #-> (fn res =>
           if name = "" andalso null locale_atts then I
-          else #2 o add_thmss kind locale [((name, locale_atts), List.concat (map #2 res'))])
+          else #2 o add_thmss kind locale [((name, locale_atts), List.concat (map #2 res))])
         #> #2
-        #> after_qed ((goal_ctxt, locale_ctxt'), raw_results) results
+        #> after_qed locale_results results
       end;
-  in global_goal (K I) kind before_qed after_qed' target (name, []) stmt elems_ctxt'' end;
+  in global_goal (K I) kind before_qed after_qed' target (name, []) stmt elems_ctxt' end;
 
 in
 
@@ -2105,9 +2120,9 @@
   gen_theorem_in_locale (K I) (K I) (K I) cert_context_statement true;
 
 fun smart_theorem kind NONE a [] concl =
-      Proof.theorem kind NONE (K (K I)) (SOME "") a concl o ProofContext.init
+      Proof.theorem kind NONE (K I) (SOME "") a concl o ProofContext.init
   | smart_theorem kind NONE a elems concl =
-      theorem kind NONE (K (K I)) a elems concl
+      theorem kind NONE (K I) a elems concl
   | smart_theorem kind (SOME loc) a elems concl =
       theorem_in_locale kind NONE (K (K I)) loc a elems concl;
 
@@ -2137,7 +2152,7 @@
 (* 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 result thy_ctxt =
+        attn all_elemss new_elemss propss thmss thy_ctxt =
     let
       fun activate_elem disch (prfx, atts) (Notes facts) thy_ctxt =
           let
@@ -2162,8 +2177,6 @@
             fold (activate_elem disch (prfx, atts2)) elems thy_ctxt
           end;
 
-      val thmss = unflat (map snd propss) result;
-
       val thy_ctxt' = thy_ctxt
         (* add registrations *)
         |> fold (fn ((id, _), _) => put_reg id attn) new_elemss
@@ -2174,12 +2187,12 @@
       val prems = List.concat (List.mapPartial
             (fn ((id, Assumed _), _) => Option.map snd (get_reg thy_ctxt' id)
               | ((_, Derived _), _) => NONE) all_elemss);
-      val disch = Drule.satisfy_hyps prems;
-      val disch' = std o Drule.fconv_rule (Thm.beta_conversion true) o disch;
+      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 disch) thms)
+        |> fold (fn (id, thms) => fold (add_wit id o apsnd disch) thms)
            (List.mapPartial (fn ((_, Assumed _), _) => NONE
               | ((id, Derived thms), _) => SOME (id, thms)) all_elemss)
     in
@@ -2194,8 +2207,9 @@
       (global_note_accesses_i (Drule.kind ""))
       Attrib.global_attribute_i Drule.standard
       (fn (name, ps) => put_global_registration (name, map Logic.varify ps))
-      (fn (n, ps) => fn thm =>
-         add_global_witness (n, map Logic.varify ps) (Drule.freeze_all thm)) x;
+      (fn (n, ps) => fn (t, th) =>
+         add_global_witness (n, map Logic.varify ps)
+         (Logic.unvarify t, Drule.freeze_all th)) x;
 
 fun local_activate_facts_elemss x = gen_activate_facts_elemss
       get_local_registration
@@ -2276,7 +2290,8 @@
     val inst_elemss = map
           (fn ((id, _), ((_, mode), elems)) =>
              inst_tab_elems thy (inst, tinst) (id, map (fn Int e => e) elems)
-               |> apfst (fn id => (id, map_mode (map (inst_tab_thm thy (inst, tinst))) mode))) 
+               |> apfst (fn id => (id, map_mode (map (fn (t, th) =>
+                 (inst_tab_term (inst, tinst) t, inst_tab_thm thy (inst, tinst) th))) mode)))
           (ids' ~~ all_elemss);
 
     (* remove fragments already registered with theory or context *)
@@ -2337,9 +2352,9 @@
     val t_ids = List.mapPartial
         (fn (id, (_, Assumed _)) => SOME id | _ => NONE) target_ids;
 
-    fun activate locale_results thy = let
-        val ids_elemss_thmss = ids_elemss ~~
-	    unflat (map snd propss) locale_results;
+    fun activate thmss thy = let
+        val satisfy = satisfy_protected (List.concat thmss);
+        val ids_elemss_thmss = ids_elemss ~~ thmss;
         val regs = get_global_registrations thy target;
 
         fun activate_id (((id, Assumed _), _), thms) thy =
@@ -2352,8 +2367,7 @@
                 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 = Drule.fconv_rule (Thm.beta_conversion true) o
-                Drule.satisfy_hyps wits;
+            val disch = satisfy_protected wits;
             val new_elemss = List.filter (fn (((name, ps), _), _) =>
                 not (test_global_registration thy (name, inst_parms ps))) (ids_elemss);
             fun activate_assumed_id (((_, Derived _), _), _) thy = thy
@@ -2364,8 +2378,9 @@
                 then thy
                 else thy
                   |> put_global_registration (name, ps') (prfx, atts2)
-                  |> fold (fn thm => fn thy => add_global_witness (name, ps')
-                       ((disch o inst_tab_thm thy (inst, tinst)) thm) thy) thms
+                  |> fold (fn (t, th) => fn thy => add_global_witness (name, ps')
+                     (inst_tab_term (inst, tinst) t,
+                      disch (inst_tab_thm thy (inst, tinst) th)) thy) thms
               end;
 
             fun activate_derived_id ((_, Assumed _), _) thy = thy
@@ -2376,8 +2391,9 @@
                 then thy
                 else thy
                   |> put_global_registration (name, ps') (prfx, atts2)
-                  |> fold (fn thm => fn thy => add_global_witness (name, ps')
-                       ((disch o inst_tab_thm thy (inst, tinst) o Drule.satisfy_hyps locale_results) thm) thy) ths
+                  |> fold (fn (t, th) => fn thy => add_global_witness (name, ps')
+                       (inst_tab_term (inst, tinst) t,
+                        disch (inst_tab_thm thy (inst, tinst) (satisfy th))) thy) ths
               end;
 
             fun activate_elem (Notes facts) thy =
@@ -2386,10 +2402,9 @@
                       |> Attrib.map_facts (Attrib.global_attribute_i thy o
                          Args.map_values I (tinst_tab_type tinst)
                            (inst_tab_term (inst, tinst))
-                           (disch o inst_tab_thm thy (inst, tinst) o
-                            Drule.satisfy_hyps locale_results))
+                           (disch o inst_tab_thm thy (inst, tinst) o satisfy))
                       |> map (apfst (apsnd (fn a => a @ map (Attrib.global_attribute thy) atts2)))
-                      |> map (apsnd (map (apfst (map (disch o inst_tab_thm thy (inst, tinst) o Drule.satisfy_hyps locale_results)))))
+                      |> map (apsnd (map (apfst (map (disch o inst_tab_thm thy (inst, tinst) o satisfy)))))
                       |> map (apfst (apfst (NameSpace.qualified prfx)))
                 in
                   fst (global_note_accesses_i (Drule.kind "") prfx facts' thy)
@@ -2409,7 +2424,15 @@
   in (propss, activate) end;
 
 fun prep_propp propss = propss |> map (fn ((name, _), props) =>
-  (("", []), map (rpair ([], [])) props));
+  (("", []), map (rpair ([], []) o Logic.protect) props));
+
+fun prep_result propps thmss =
+  ListPair.map (fn ((_, props), thms) => (props ~~ thms)) (propps, thmss);
+
+val refine_protected =
+  Proof.refine (Method.Basic (K (Method.METHOD   (* FIXME avoid conjunction_tac (!?) *)
+    (K (ALLGOALS (Tactic.rtac Drule.protectI))))))
+  #> Seq.hd;
 
 fun goal_name thy kind target propss =
     kind ^ Proof.goal_names (Option.map (extern thy) target) ""
@@ -2422,31 +2445,39 @@
     val thy_ctxt = ProofContext.init thy;
     val (propss, activate) = prep_global_registration (prfx, atts) expr insts thy;
     val kind = goal_name thy "interpretation" NONE propss;
-    fun after_qed (goal_ctxt, raw_results) _ =
-      activate (map (ProofContext.export_plain goal_ctxt thy_ctxt) raw_results);
-  in Proof.theorem_i kind NONE after_qed NONE ("", []) (prep_propp propss) thy_ctxt end;
+    fun after_qed results = activate (prep_result propss results);
+  in
+    thy_ctxt
+    |> Proof.theorem_i kind NONE after_qed NONE ("", []) (prep_propp propss)
+    |> refine_protected
+  end;
 
 fun interpretation_in_locale (raw_target, expr) thy =
   let
     val target = intern thy raw_target;
     val (propss, activate) = prep_registration_in_locale target expr thy;
     val kind = goal_name thy "interpretation" (SOME target) propss;
-    fun after_qed ((goal_ctxt, locale_ctxt), raw_results) _ =
-      activate (map (ProofContext.export_plain goal_ctxt locale_ctxt) raw_results);
-  in theorem_in_locale_no_target kind NONE after_qed target ("", []) [] (prep_propp propss) thy end;
+    fun after_qed locale_results _ = activate (prep_result propss locale_results);
+  in
+    thy
+    |> theorem_in_locale_no_target kind NONE after_qed target ("", []) [] (prep_propp propss)
+    |> refine_protected
+  end;
 
 fun interpret (prfx, atts) expr insts int state =
   let
     val ctxt = Proof.context_of state;
     val (propss, activate) = prep_local_registration (prfx, atts) expr insts ctxt;
     val kind = goal_name (Proof.theory_of state) "interpret" NONE propss;
-    fun after_qed (_, raw_results) _ =
-      Proof.map_context (K (ctxt |> activate raw_results))
+    fun after_qed results =
+      Proof.map_context (K (ctxt |> activate (prep_result propss results)))
       #> Proof.put_facts NONE
       #> Seq.single;
   in
-    Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
-      kind NONE after_qed (prep_propp propss) state
+    state
+    |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
+      kind NONE after_qed (prep_propp propss)
+    |> refine_protected
   end;
 
 end;