# HG changeset patch
# User wenzelm
# Date 1518862288 -3600
# Node ID 967c16e9c724599d03a028547849aeeaf15613bc
# Parent  3817a93a3e5e3299bec5096b9658ca0fcf8287f3# Parent  fb4b2b6333710a8c202f5328609f3b687d4680aa
merged

diff -r 3817a93a3e5e -r 967c16e9c724 src/HOL/Nonstandard_Analysis/StarDef.thy
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Sat Feb 17 11:11:28 2018 +0100
@@ -99,7 +99,7 @@
   where "star_of x \<equiv> star_n (\<lambda>n. x)"
 
 text \<open>Initialize transfer tactic.\<close>
-ML_file "transfer.ML"
+ML_file "transfer_principle.ML"
 
 method_setup transfer =
   \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (Transfer_Principle.transfer_tac ctxt ths))\<close>
diff -r 3817a93a3e5e -r 967c16e9c724 src/HOL/Nonstandard_Analysis/transfer.ML
--- a/src/HOL/Nonstandard_Analysis/transfer.ML	Sat Feb 03 09:11:21 2018 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,135 +0,0 @@
-(*  Title:      HOL/Nonstandard_Analysis/transfer.ML
-    Author:     Brian Huffman
-
-Transfer principle tactic for nonstandard analysis.
-*)
-
-signature TRANSFER_PRINCIPLE =
-sig
-  val transfer_tac: Proof.context -> thm list -> int -> tactic
-  val add_const: string -> theory -> theory
-end;
-
-structure Transfer_Principle: TRANSFER_PRINCIPLE =
-struct
-
-structure Data = Generic_Data
-(
-  type T = {
-    intros: thm list,
-    unfolds: thm list,
-    refolds: thm list,
-    consts: string list
-  };
-  val empty = {intros = [], unfolds = [], refolds = [], consts = []};
-  val extend = I;
-  fun merge
-    ({intros = intros1, unfolds = unfolds1,
-      refolds = refolds1, consts = consts1},
-     {intros = intros2, unfolds = unfolds2,
-      refolds = refolds2, consts = consts2}) : T =
-   {intros = Thm.merge_thms (intros1, intros2),
-    unfolds = Thm.merge_thms (unfolds1, unfolds2),
-    refolds = Thm.merge_thms (refolds1, refolds2),
-    consts = Library.merge (op =) (consts1, consts2)};
-);
-
-fun unstar_typ (Type (@{type_name star}, [t])) = unstar_typ t
-  | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
-  | unstar_typ T = T
-
-fun unstar_term consts term =
-  let
-    fun unstar (Const(a,T) $ t) = if member (op =) consts a then (unstar t)
-          else (Const(a,unstar_typ T) $ unstar t)
-      | unstar (f $ t) = unstar f $ unstar t
-      | unstar (Const(a,T)) = Const(a,unstar_typ T)
-      | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t)
-      | unstar t = t
-  in
-    unstar term
-  end
-
-local exception MATCH
-in
-fun transfer_star_tac ctxt =
-  let
-    fun thm_of (Const (@{const_name Ifun}, _) $ t $ u) = @{thm transfer_Ifun} OF [thm_of t, thm_of u]
-      | thm_of (Const (@{const_name star_of}, _) $ _) = @{thm star_of_def}
-      | thm_of (Const (@{const_name star_n}, _) $ _) = @{thm Pure.reflexive}
-      | thm_of _ = raise MATCH;
-
-    fun thm_of_goal (Const (@{const_name Pure.eq}, _) $ t $ (Const (@{const_name star_n}, _) $ _)) =
-          thm_of t
-      | thm_of_goal _ = raise MATCH;
-  in
-    SUBGOAL (fn (t, i) =>
-      resolve_tac ctxt [thm_of_goal (strip_all_body t |> Logic.strip_imp_concl)] i
-      handle MATCH => no_tac)
-  end;
-end;
-
-fun transfer_thm_of ctxt ths t =
-  let
-    val {intros,unfolds,refolds,consts} = Data.get (Context.Proof ctxt);
-    val meta = Local_Defs.meta_rewrite_rule ctxt;
-    val ths' = map meta ths;
-    val unfolds' = map meta unfolds and refolds' = map meta refolds;
-    val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (Thm.cterm_of ctxt t))
-    val u = unstar_term consts t'
-    val tac =
-      rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
-      ALLGOALS (Object_Logic.full_atomize_tac ctxt) THEN
-      match_tac ctxt [transitive_thm] 1 THEN
-      resolve_tac ctxt [@{thm transfer_start}] 1 THEN
-      REPEAT_ALL_NEW (resolve_tac ctxt intros ORELSE' transfer_star_tac ctxt) 1 THEN
-      match_tac ctxt [reflexive_thm] 1
-  in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end;
-
-fun transfer_tac ctxt ths = SUBGOAL (fn (t, _) => (fn th =>
-  let
-    val tr = transfer_thm_of ctxt ths t
-    val (_$ l $ r) = Thm.concl_of tr;
-    val trs = if l aconv r then [] else [tr];
-  in rewrite_goals_tac ctxt trs th end));
-
-local
-
-fun map_intros f = Data.map
-  (fn {intros,unfolds,refolds,consts} =>
-    {intros=f intros, unfolds=unfolds, refolds=refolds, consts=consts})
-
-fun map_unfolds f = Data.map
-  (fn {intros,unfolds,refolds,consts} =>
-    {intros=intros, unfolds=f unfolds, refolds=refolds, consts=consts})
-
-fun map_refolds f = Data.map
-  (fn {intros,unfolds,refolds,consts} =>
-    {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts})
-in
-
-val intro_add = Thm.declaration_attribute (map_intros o Thm.add_thm);
-val intro_del = Thm.declaration_attribute (map_intros o Thm.del_thm);
-
-val unfold_add = Thm.declaration_attribute (map_unfolds o Thm.add_thm);
-val unfold_del = Thm.declaration_attribute (map_unfolds o Thm.del_thm);
-
-val refold_add = Thm.declaration_attribute (map_refolds o Thm.add_thm);
-val refold_del = Thm.declaration_attribute (map_refolds o Thm.del_thm);
-
-end
-
-fun add_const c = Context.theory_map (Data.map
-  (fn {intros,unfolds,refolds,consts} =>
-    {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
-
-val _ =
-  Theory.setup
-   (Attrib.setup @{binding transfer_intro} (Attrib.add_del intro_add intro_del)
-      "declaration of transfer introduction rule" #>
-    Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del)
-      "declaration of transfer unfolding rule" #>
-    Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del)
-      "declaration of transfer refolding rule")
-
-end;
diff -r 3817a93a3e5e -r 967c16e9c724 src/HOL/Nonstandard_Analysis/transfer_principle.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Nonstandard_Analysis/transfer_principle.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -0,0 +1,135 @@
+(*  Title:      HOL/Nonstandard_Analysis/transfer_principle.ML
+    Author:     Brian Huffman
+
+Transfer principle tactic for nonstandard analysis.
+*)
+
+signature TRANSFER_PRINCIPLE =
+sig
+  val transfer_tac: Proof.context -> thm list -> int -> tactic
+  val add_const: string -> theory -> theory
+end;
+
+structure Transfer_Principle: TRANSFER_PRINCIPLE =
+struct
+
+structure Data = Generic_Data
+(
+  type T = {
+    intros: thm list,
+    unfolds: thm list,
+    refolds: thm list,
+    consts: string list
+  };
+  val empty = {intros = [], unfolds = [], refolds = [], consts = []};
+  val extend = I;
+  fun merge
+    ({intros = intros1, unfolds = unfolds1,
+      refolds = refolds1, consts = consts1},
+     {intros = intros2, unfolds = unfolds2,
+      refolds = refolds2, consts = consts2}) : T =
+   {intros = Thm.merge_thms (intros1, intros2),
+    unfolds = Thm.merge_thms (unfolds1, unfolds2),
+    refolds = Thm.merge_thms (refolds1, refolds2),
+    consts = Library.merge (op =) (consts1, consts2)};
+);
+
+fun unstar_typ (Type (@{type_name star}, [t])) = unstar_typ t
+  | unstar_typ (Type (a, Ts)) = Type (a, map unstar_typ Ts)
+  | unstar_typ T = T
+
+fun unstar_term consts term =
+  let
+    fun unstar (Const(a,T) $ t) = if member (op =) consts a then (unstar t)
+          else (Const(a,unstar_typ T) $ unstar t)
+      | unstar (f $ t) = unstar f $ unstar t
+      | unstar (Const(a,T)) = Const(a,unstar_typ T)
+      | unstar (Abs(a,T,t)) = Abs(a,unstar_typ T,unstar t)
+      | unstar t = t
+  in
+    unstar term
+  end
+
+local exception MATCH
+in
+fun transfer_star_tac ctxt =
+  let
+    fun thm_of (Const (@{const_name Ifun}, _) $ t $ u) = @{thm transfer_Ifun} OF [thm_of t, thm_of u]
+      | thm_of (Const (@{const_name star_of}, _) $ _) = @{thm star_of_def}
+      | thm_of (Const (@{const_name star_n}, _) $ _) = @{thm Pure.reflexive}
+      | thm_of _ = raise MATCH;
+
+    fun thm_of_goal (Const (@{const_name Pure.eq}, _) $ t $ (Const (@{const_name star_n}, _) $ _)) =
+          thm_of t
+      | thm_of_goal _ = raise MATCH;
+  in
+    SUBGOAL (fn (t, i) =>
+      resolve_tac ctxt [thm_of_goal (strip_all_body t |> Logic.strip_imp_concl)] i
+      handle MATCH => no_tac)
+  end;
+end;
+
+fun transfer_thm_of ctxt ths t =
+  let
+    val {intros,unfolds,refolds,consts} = Data.get (Context.Proof ctxt);
+    val meta = Local_Defs.meta_rewrite_rule ctxt;
+    val ths' = map meta ths;
+    val unfolds' = map meta unfolds and refolds' = map meta refolds;
+    val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (Thm.cterm_of ctxt t))
+    val u = unstar_term consts t'
+    val tac =
+      rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
+      ALLGOALS (Object_Logic.full_atomize_tac ctxt) THEN
+      match_tac ctxt [transitive_thm] 1 THEN
+      resolve_tac ctxt [@{thm transfer_start}] 1 THEN
+      REPEAT_ALL_NEW (resolve_tac ctxt intros ORELSE' transfer_star_tac ctxt) 1 THEN
+      match_tac ctxt [reflexive_thm] 1
+  in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end;
+
+fun transfer_tac ctxt ths = SUBGOAL (fn (t, _) => (fn th =>
+  let
+    val tr = transfer_thm_of ctxt ths t
+    val (_$ l $ r) = Thm.concl_of tr;
+    val trs = if l aconv r then [] else [tr];
+  in rewrite_goals_tac ctxt trs th end));
+
+local
+
+fun map_intros f = Data.map
+  (fn {intros,unfolds,refolds,consts} =>
+    {intros=f intros, unfolds=unfolds, refolds=refolds, consts=consts})
+
+fun map_unfolds f = Data.map
+  (fn {intros,unfolds,refolds,consts} =>
+    {intros=intros, unfolds=f unfolds, refolds=refolds, consts=consts})
+
+fun map_refolds f = Data.map
+  (fn {intros,unfolds,refolds,consts} =>
+    {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts})
+in
+
+val intro_add = Thm.declaration_attribute (map_intros o Thm.add_thm o Thm.trim_context);
+val intro_del = Thm.declaration_attribute (map_intros o Thm.del_thm);
+
+val unfold_add = Thm.declaration_attribute (map_unfolds o Thm.add_thm o Thm.trim_context);
+val unfold_del = Thm.declaration_attribute (map_unfolds o Thm.del_thm);
+
+val refold_add = Thm.declaration_attribute (map_refolds o Thm.add_thm o Thm.trim_context);
+val refold_del = Thm.declaration_attribute (map_refolds o Thm.del_thm);
+
+end
+
+fun add_const c = Context.theory_map (Data.map
+  (fn {intros,unfolds,refolds,consts} =>
+    {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
+
+val _ =
+  Theory.setup
+   (Attrib.setup @{binding transfer_intro} (Attrib.add_del intro_add intro_del)
+      "declaration of transfer introduction rule" #>
+    Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del)
+      "declaration of transfer unfolding rule" #>
+    Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del)
+      "declaration of transfer refolding rule")
+
+end;
diff -r 3817a93a3e5e -r 967c16e9c724 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/Function/function.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -6,7 +6,7 @@
 
 signature FUNCTION =
 sig
-  include FUNCTION_DATA
+  type info = Function_Common.info
 
   val add_function: (binding * typ option * mixfix) list ->
     Specification.multi_specs -> Function_Common.function_config ->
@@ -266,7 +266,7 @@
 
 val get_congs = Function_Context_Tree.get_function_congs
 
-fun get_info ctxt t = Item_Net.retrieve (get_functions ctxt) t
+fun get_info ctxt t = Function_Common.retrieve_function_data ctxt t
   |> the_single |> snd
 
 
diff -r 3817a93a3e5e -r 967c16e9c724 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/Function/function_common.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -4,7 +4,7 @@
 Common definitions and other infrastructure for the function package.
 *)
 
-signature FUNCTION_DATA =
+signature FUNCTION_COMMON =
 sig
   type info =
    {is_partial : bool,
@@ -26,37 +26,6 @@
     cases : thm list,
     pelims: thm list list,
     elims: thm list list option}
-end
-
-structure Function_Data : FUNCTION_DATA =
-struct
-
-type info =
- {is_partial : bool,
-  defname : binding,
-    (*contains no logical entities: invariant under morphisms:*)
-  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
-    Token.src list -> thm list -> local_theory -> thm list * local_theory,
-  fnames : binding list,
-  case_names : string list,
-  fs : term list,
-  R : term,
-  dom: term,
-  psimps: thm list,
-  pinducts: thm list,
-  simps : thm list option,
-  inducts : thm list option,
-  termination : thm,
-  totality : thm option,
-  cases : thm list,
-  pelims : thm list list,
-  elims : thm list list option}
-
-end
-
-signature FUNCTION_COMMON =
-sig
-  include FUNCTION_DATA
   val profile : bool Unsynchronized.ref
   val PROFILE : string -> ('a -> 'b) -> 'a -> 'b
   val mk_acc : typ -> term -> term
@@ -78,7 +47,7 @@
     preproc
   val termination_rule_tac : Proof.context -> int -> tactic
   val store_termination_rule : thm -> Context.generic -> Context.generic
-  val get_functions : Proof.context -> (term * info) Item_Net.T
+  val retrieve_function_data : Proof.context -> term -> (term * info) list
   val add_function_data : info -> Context.generic -> Context.generic
   val termination_prover_tac : bool -> Proof.context -> tactic
   val set_termination_prover : (bool -> Proof.context -> tactic) -> Context.generic ->
@@ -107,9 +76,46 @@
 structure Function_Common : FUNCTION_COMMON =
 struct
 
-open Function_Data
+local open Function_Lib in
+
+(* info *)
 
-local open Function_Lib in
+type info =
+ {is_partial : bool,
+  defname : binding,
+    (*contains no logical entities: invariant under morphisms:*)
+  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
+    Token.src list -> thm list -> local_theory -> thm list * local_theory,
+  fnames : binding list,
+  case_names : string list,
+  fs : term list,
+  R : term,
+  dom: term,
+  psimps: thm list,
+  pinducts: thm list,
+  simps : thm list option,
+  inducts : thm list option,
+  termination : thm,
+  totality : thm option,
+  cases : thm list,
+  pelims : thm list list,
+  elims : thm list list option}
+
+fun transform_function_data phi ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
+  simps, inducts, termination, totality, defname, is_partial, cases, pelims, elims} : info) =
+    let
+      val term = Morphism.term phi
+      val thm = Morphism.thm phi
+      val fact = Morphism.fact phi
+    in
+      { add_simps = add_simps, case_names = case_names, fnames = fnames,
+        fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
+        pinducts = fact pinducts, simps = Option.map fact simps,
+        inducts = Option.map fact inducts, termination = thm termination,
+        totality = Option.map thm totality, defname = Morphism.binding phi defname,
+        is_partial = is_partial, cases = fact cases,
+        elims = Option.map (map fact) elims, pelims = map fact pelims }
+    end
 
 
 (* profiling *)
@@ -267,9 +273,17 @@
 val store_termination_rule = Data.map o @{apply 4(1)} o cons o Thm.trim_context
 
 val get_functions = #2 o Data.get o Context.Proof
-fun add_function_data (info : info as {fs, termination, ...}) =
-  (Data.map o @{apply 4(2)}) (fold (fn f => Item_Net.update (f, info)) fs)
-  #> store_termination_rule termination
+
+fun retrieve_function_data ctxt t =
+  Item_Net.retrieve (get_functions ctxt) t
+  |> (map o apsnd)
+      (transform_function_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
+
+val add_function_data =
+  transform_function_data Morphism.trim_context_morphism #>
+  (fn info as {fs, termination, ...} =>
+    (Data.map o @{apply 4(2)}) (fold (fn f => Item_Net.update (f, info)) fs)
+    #> store_termination_rule termination)
 
 fun termination_prover_tac quiet ctxt = #3 (Data.get (Context.Proof ctxt)) quiet ctxt
 val set_termination_prover = Data.map o @{apply 4(3)} o K
@@ -292,22 +306,6 @@
   termination : thm,
   domintros : thm list option}
 
-fun transform_function_data phi ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
-  simps, inducts, termination, totality, defname, is_partial, cases, pelims, elims} : info) =
-    let
-      val term = Morphism.term phi
-      val thm = Morphism.thm phi
-      val fact = Morphism.fact phi
-    in
-      { add_simps = add_simps, case_names = case_names, fnames = fnames,
-        fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
-        pinducts = fact pinducts, simps = Option.map fact simps,
-        inducts = Option.map fact inducts, termination = thm termination,
-        totality = Option.map thm totality, defname = Morphism.binding phi defname,
-        is_partial = is_partial, cases = fact cases,
-        elims = Option.map (map fact) elims, pelims = map fact pelims }
-    end
-
 fun lift_morphism ctxt f =
   let
     fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of ctxt t))
@@ -328,7 +326,7 @@
       SOME (transform_function_data (inst_morph (Thm.match (Thm.cterm_of ctxt trm, ct))) data)
         handle Pattern.MATCH => NONE
   in
-    get_first match (Item_Net.retrieve (get_functions ctxt) t)
+    get_first match (retrieve_function_data ctxt t)
   end
 
 fun import_last_function ctxt =
diff -r 3817a93a3e5e -r 967c16e9c724 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -61,11 +61,11 @@
     val (_, prop') = Local_Defs.cert_def lthy (K []) prop
     val (_, newrhs) = Local_Defs.abs_def prop'
 
-    val ((trm, (_ , def_thm)), lthy') =
+    val ((qconst, (_ , def)), lthy') =
       Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy
 
-    (* data storage *)
-    val qconst_data = {qconst = trm, rconst = rhs, def = def_thm}
+    fun qconst_data phi =
+      Quotient_Info.transform_quotconsts phi {qconst = qconst, rconst = rhs, def = def}
 
     fun qualify defname suffix = Binding.name suffix
       |> Binding.qualify true defname
@@ -76,14 +76,14 @@
     val lthy'' = lthy'
       |> Local_Theory.declaration {syntax = false, pervasive = true}
         (fn phi =>
-          (case Quotient_Info.transform_quotconsts phi qconst_data of
+          (case qconst_data phi of
             qcinfo as {qconst = Const (c, _), ...} =>
               Quotient_Info.update_quotconsts (c, qcinfo)
           | _ => I))
       |> (snd oo Local_Theory.note)
         ((rsp_thm_name, @{attributes [quot_respect]}), [rsp_thm])
   in
-    (qconst_data, lthy'')
+    (qconst_data Morphism.identity, lthy'')
   end
 
 fun mk_readable_rsp_thm_eq tm lthy =
diff -r 3817a93a3e5e -r 967c16e9c724 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -9,6 +9,7 @@
   type quotmaps = {relmap: string, quot_thm: thm}
   val lookup_quotmaps: Proof.context -> string -> quotmaps option
   val lookup_quotmaps_global: theory -> string -> quotmaps option
+  val update_quotmaps: string * quotmaps -> Context.generic -> Context.generic
   val print_quotmaps: Proof.context -> unit
 
   type abs_rep = {abs : term, rep : term}
@@ -30,10 +31,10 @@
   val transform_quotconsts: morphism -> quotconsts -> quotconsts
   val lookup_quotconsts_global: theory -> term -> quotconsts option
   val update_quotconsts: string * quotconsts -> Context.generic -> Context.generic
+  val dest_quotconsts: Proof.context -> quotconsts list
   val dest_quotconsts_global: theory -> quotconsts list
-  val dest_quotconsts: Proof.context -> quotconsts list
   val print_quotconsts: Proof.context -> unit
-end;
+end
 
 structure Quotient_Info: QUOTIENT_INFO =
 struct
@@ -42,20 +43,23 @@
 
 (*info about map- and rel-functions for a type*)
 type quotmaps = {relmap: string, quot_thm: thm}
+fun transform_quotmaps phi : quotmaps -> quotmaps =
+  fn {relmap, quot_thm} => {relmap = relmap, quot_thm = Morphism.thm phi quot_thm}
 
 (*info about abs/rep terms*)
 type abs_rep = {abs : term, rep : term}
-fun transform_abs_rep phi {abs, rep} : abs_rep =
-  {abs = Morphism.term phi abs, rep = Morphism.term phi rep}
+fun transform_abs_rep phi : abs_rep -> abs_rep =
+  fn {abs, rep} => {abs = Morphism.term phi abs, rep = Morphism.term phi rep}
 
 (*info about quotient types*)
 type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
-fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} : quotients =
-  {qtyp = Morphism.typ phi qtyp,
-   rtyp = Morphism.typ phi rtyp,
-   equiv_rel = Morphism.term phi equiv_rel,
-   equiv_thm = Morphism.thm phi equiv_thm,
-   quot_thm = Morphism.thm phi quot_thm}
+fun transform_quotients phi : quotients -> quotients =
+  fn {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =>
+    {qtyp = Morphism.typ phi qtyp,
+     rtyp = Morphism.typ phi rtyp,
+     equiv_rel = Morphism.term phi equiv_rel,
+     equiv_thm = Morphism.thm phi equiv_thm,
+     quot_thm = Morphism.thm phi quot_thm}
 
 (*info about quotient constants*)
 (*We need to be able to lookup instances of lifted constants,
@@ -63,10 +67,11 @@
   but overloaded constants share the same name.*)
 type quotconsts = {qconst: term, rconst: term, def: thm}
 fun eq_quotconsts (x: quotconsts, y: quotconsts) = #qconst x = #qconst y
-fun transform_quotconsts phi {qconst, rconst, def} : quotconsts =
-  {qconst = Morphism.term phi qconst,
-   rconst = Morphism.term phi rconst,
-   def = Morphism.thm phi def}
+fun transform_quotconsts phi : quotconsts -> quotconsts =
+  fn {qconst, rconst, def} =>
+    {qconst = Morphism.term phi qconst,
+     rconst = Morphism.term phi rconst,
+     def = Morphism.thm phi def}
 
 structure Data = Generic_Data
 (
@@ -99,10 +104,15 @@
 
 (* quotmaps *)
 
-val lookup_quotmaps = Symtab.lookup o get_quotmaps o Context.Proof
-val lookup_quotmaps_global = Symtab.lookup o get_quotmaps o Context.Theory
+fun lookup_quotmaps_generic context name =
+  Symtab.lookup (get_quotmaps context) name
+  |> Option.map (transform_quotmaps (Morphism.transfer_morphism (Context.theory_of context)))
 
-(* FIXME export proper internal update operation!? *)
+val lookup_quotmaps = lookup_quotmaps_generic o Context.Proof
+val lookup_quotmaps_global = lookup_quotmaps_generic o Context.Theory
+
+val update_quotmaps =
+  map_quotmaps o Symtab.update o apsnd (transform_quotmaps Morphism.trim_context_morphism)
 
 val _ =
   Theory.setup
@@ -111,9 +121,9 @@
         (Scan.lift @{keyword "("} |--
           Args.const {proper = true, strict = true} --| Scan.lift @{keyword ","} --
           Attrib.thm --| Scan.lift @{keyword ")"}) >>
-        (fn (tyname, (relname, qthm)) =>
-          let val minfo = {relmap = relname, quot_thm = qthm}
-          in Thm.declaration_attribute (fn _ => map_quotmaps (Symtab.update (tyname, minfo))) end))
+        (fn (tyname, (relmap, quot_thm)) =>
+          Thm.declaration_attribute
+            (K (update_quotmaps (tyname, {relmap = relmap, quot_thm = quot_thm})))))
       "declaration of map information")
 
 fun print_quotmaps ctxt =
@@ -138,7 +148,8 @@
 val lookup_abs_rep = Symtab.lookup o get_abs_rep o Context.Proof
 val lookup_abs_rep_global = Symtab.lookup o get_abs_rep o Context.Theory
 
-val update_abs_rep = map_abs_rep o Symtab.update
+val update_abs_rep =
+  map_abs_rep o Symtab.update o apsnd (transform_abs_rep Morphism.trim_context_morphism)
 
 fun print_abs_rep ctxt =
   let
@@ -159,10 +170,15 @@
 
 (* quotients *)
 
-val lookup_quotients = Symtab.lookup o get_quotients o Context.Proof
-val lookup_quotients_global = Symtab.lookup o get_quotients o Context.Theory
+fun lookup_quotients_generic context name =
+  Symtab.lookup (get_quotients context) name
+  |> Option.map (transform_quotients (Morphism.transfer_morphism (Context.theory_of context)))
 
-val update_quotients = map_quotients o Symtab.update
+val lookup_quotients = lookup_quotients_generic o Context.Proof
+val lookup_quotients_global = lookup_quotients_generic o Context.Theory
+
+val update_quotients =
+  map_quotients o Symtab.update o apsnd (transform_quotients Morphism.trim_context_morphism)
 
 fun dest_quotients ctxt =
   map snd (Symtab.dest (get_quotients (Context.Proof ctxt)))
@@ -190,24 +206,25 @@
 
 (* quotconsts *)
 
-val update_quotconsts = map_quotconsts o Symtab.cons_list
+val update_quotconsts =
+  map_quotconsts o Symtab.cons_list o apsnd (transform_quotconsts Morphism.trim_context_morphism)
 
-fun dest_quotconsts ctxt =
-  maps snd (Symtab.dest (get_quotconsts (Context.Proof ctxt)))
+fun dest_quotconsts_generic context =
+  maps #2 (Symtab.dest (get_quotconsts context))
+  |> map (transform_quotconsts (Morphism.transfer_morphism (Context.theory_of context)))
 
-fun dest_quotconsts_global thy =
-  maps snd (Symtab.dest (get_quotconsts (Context.Theory thy)))
+val dest_quotconsts = dest_quotconsts_generic o Context.Proof
+val dest_quotconsts_global = dest_quotconsts_generic o Context.Theory
 
 fun lookup_quotconsts_global thy t =
   let
     val (name, qty) = dest_Const t
-    fun matches (x: quotconsts) =
-      let val (name', qty') = dest_Const (#qconst x);
-      in name = name' andalso Sign.typ_instance thy (qty, qty') end
   in
-    (case Symtab.lookup (get_quotconsts (Context.Theory thy)) name of
-      NONE => NONE
-    | SOME l => find_first matches l)
+    Symtab.lookup_list (get_quotconsts (Context.Theory thy)) name
+    |> find_first (fn {qconst, ...} =>
+        let val (name', qty') = dest_Const qconst
+        in name = name' andalso Sign.typ_instance thy (qty, qty') end)
+    |> Option.map (transform_quotconsts (Morphism.transfer_morphism thy))
   end
 
 fun print_quotconsts ctxt =
@@ -220,7 +237,7 @@
         Pretty.str "as",
         Syntax.pretty_term ctxt (Thm.prop_of def)])
   in
-    map prt_qconst (maps snd (Symtab.dest (get_quotconsts (Context.Proof ctxt))))
+    map prt_qconst (dest_quotconsts ctxt)
     |> Pretty.big_list "quotient constants:"
     |> Pretty.writeln
   end
@@ -240,4 +257,4 @@
   Outer_Syntax.command @{command_keyword print_quotconsts} "print quotient constants"
     (Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
 
-end;
+end
diff -r 3817a93a3e5e -r 967c16e9c724 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -154,7 +154,6 @@
 
 fun regularize_tac ctxt =
   let
-    val thy = Proof_Context.theory_of ctxt
     val simpset =
       mk_minimal_simpset ctxt
       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
diff -r 3817a93a3e5e -r 967c16e9c724 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -83,7 +83,7 @@
     val thy = Proof_Context.theory_of ctxt
   in
     (case Quotient_Info.lookup_quotients_global thy s of
-      SOME qdata => (#rtyp qdata, #qtyp qdata)
+      SOME {rtyp, qtyp, ...} => (rtyp, qtyp)
     | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
   end
 
@@ -104,12 +104,9 @@
       | mk_dummyT (Free (c, _)) = Free (c, dummyT)
       | mk_dummyT _ = error "Expecting abs/rep term to be a constant or a free variable"     
   in
-    case Quotient_Info.lookup_abs_rep ctxt qty_str of
-      SOME abs_rep => 
-        mk_dummyT (case flag of
-          AbsF => #abs abs_rep
-        | RepF => #rep abs_rep)
-      | NONE => error ("No abs/rep terms for " ^ quote qty_str)
+    (case Quotient_Info.lookup_abs_rep ctxt qty_str of
+      SOME {abs, rep} => mk_dummyT (case flag of AbsF => abs | RepF => rep)
+    | NONE => error ("No abs/rep terms for " ^ quote qty_str))
   end
   
 (* Lets Nitpick represent elements of quotient types as elements of the raw type *)
@@ -273,14 +270,14 @@
 fun mk_rel_compose (trm1, trm2) =
   Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2
 
-fun get_relmap thy s =
-  (case Quotient_Info.lookup_quotmaps thy s of
-    SOME map_data => Const (#relmap map_data, dummyT)
+fun get_relmap ctxt s =
+  (case Quotient_Info.lookup_quotmaps ctxt s of
+    SOME {relmap, ...} => Const (relmap, dummyT)
   | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"))
 
-fun get_equiv_rel thy s =
-  (case Quotient_Info.lookup_quotients thy s of
-    SOME qdata => #equiv_rel qdata
+fun get_equiv_rel ctxt s =
+  (case Quotient_Info.lookup_quotients ctxt s of
+    SOME {equiv_rel, ...} => equiv_rel
   | NONE => raise LIFT_MATCH ("get_equiv_rel (no quotient found for type " ^ s ^ ")"))
 
 fun equiv_match_err ctxt ty_pat ty =
@@ -338,22 +335,14 @@
 exception CODE_GEN of string
 
 fun get_quot_thm ctxt s =
-  let
-    val thy = Proof_Context.theory_of ctxt
-  in
-    (case Quotient_Info.lookup_quotients ctxt s of
-      SOME qdata => Thm.transfer thy (#quot_thm qdata)
-    | NONE => raise CODE_GEN ("No quotient type " ^ quote s ^ " found."))
-  end
+  (case Quotient_Info.lookup_quotients ctxt s of
+    SOME {quot_thm, ...} => quot_thm
+  | NONE => raise CODE_GEN ("No quotient type " ^ quote s ^ " found."));
 
 fun get_rel_quot_thm ctxt s =
-   let
-    val thy = Proof_Context.theory_of ctxt
-  in
-    (case Quotient_Info.lookup_quotmaps ctxt s of
-      SOME map_data => Thm.transfer thy (#quot_thm map_data)
-    | NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")"))
-  end
+  (case Quotient_Info.lookup_quotmaps ctxt s of
+    SOME {quot_thm, ...} => quot_thm
+  | NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")"));
 
 fun is_id_quot thm = Thm.eq_thm_prop (thm, @{thm identity_quotient3})
 
@@ -497,7 +486,7 @@
             else forall (fn x => x = true) (map2 (matches_typ ctxt) rtys qtys)
           else
             (case Quotient_Info.lookup_quotients_global thy qs of
-              SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
+              SOME {rtyp, ...} => Sign.typ_instance thy (rT, rtyp)
             | NONE => false)
       | _ => false)
   end
@@ -626,7 +615,7 @@
           let
             val rtrm' =
               (case Quotient_Info.lookup_quotconsts_global thy qtrm of
-                SOME qconst_info => #rconst qconst_info
+                SOME {rconst, ...} => rconst
               | NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm)
           in
             if Pattern.matches thy (rtrm', rtrm)
@@ -858,5 +847,4 @@
 fun derive_rtrm ctxt qtys qtrm =
   subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm
 
-
 end;
diff -r 3817a93a3e5e -r 967c16e9c724 src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -141,17 +141,18 @@
     val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o Thm.prop_of) quot_thm
     val (qtyp, rtyp) = (dest_funT o fastype_of) rep
     val qty_full_name = (fst o dest_Type) qtyp
-    val quotients = {qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm,
-      quot_thm = quot_thm }
-    fun quot_info phi = Quotient_Info.transform_quotients phi quotients
-    val abs_rep = {abs = abs, rep = rep}
-    fun abs_rep_info phi = Quotient_Info.transform_abs_rep phi abs_rep
+    fun quotients phi =
+      Quotient_Info.transform_quotients phi
+        {qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm,
+          quot_thm = quot_thm}
+    fun abs_rep phi =
+      Quotient_Info.transform_abs_rep phi {abs = abs, rep = rep}
   in
     lthy
-      |> Local_Theory.declaration {syntax = false, pervasive = true}
-        (fn phi => Quotient_Info.update_quotients (qty_full_name, quot_info phi)
-          #> Quotient_Info.update_abs_rep (qty_full_name, abs_rep_info phi))
-      |> setup_lifting_package quot_thm equiv_thm opt_par_thm
+    |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
+        Quotient_Info.update_quotients (qty_full_name, quotients phi) #>
+        Quotient_Info.update_abs_rep (qty_full_name, abs_rep phi))
+    |> setup_lifting_package quot_thm equiv_thm opt_par_thm
   end
 
 (* main function for constructing a quotient type *)
diff -r 3817a93a3e5e -r 967c16e9c724 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/inductive.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -257,21 +257,26 @@
 fun the_inductive ctxt term =
   Item_Net.retrieve (#infos (rep_data ctxt)) term
   |> the_single
+  |> apsnd (transform_result (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
 
 fun the_inductive_global ctxt name =
   #infos (rep_data ctxt)
   |> Item_Net.content
   |> filter (fn ({names, ...}, _) => member op = names name)
   |> the_single
+  |> apsnd (transform_result (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))
 
 fun put_inductives info =
   map_data (fn (infos, monos, equations) =>
-    (Item_Net.update info infos, monos, equations));
+    (Item_Net.update (apsnd (transform_result Morphism.trim_context_morphism) info) infos,
+      monos, equations));
 
 
 (* monotonicity rules *)
 
-val get_monos = #monos o rep_data;
+fun get_monos ctxt =
+  #monos (rep_data ctxt)
+  |> map (Thm.transfer (Proof_Context.theory_of ctxt));
 
 fun mk_mono ctxt thm =
   let
@@ -291,7 +296,8 @@
 val mono_add =
   Thm.declaration_attribute (fn thm => fn context =>
     map_data (fn (infos, monos, equations) =>
-      (infos, Thm.add_thm (mk_mono (Context.proof_of context) thm) monos, equations)) context);
+      (infos, Thm.add_thm (Thm.trim_context (mk_mono (Context.proof_of context) thm)) monos,
+        equations)) context);
 
 val mono_del =
   Thm.declaration_attribute (fn thm => fn context =>
@@ -306,12 +312,14 @@
 
 (* equations *)
 
-val get_equations = #equations o rep_data;
+fun retrieve_equations ctxt =
+  Item_Net.retrieve (#equations (rep_data ctxt))
+  #> map (Thm.transfer (Proof_Context.theory_of ctxt));
 
 val equation_add_permissive =
   Thm.declaration_attribute (fn thm =>
     map_data (fn (infos, monos, equations) =>
-      (infos, monos, perhaps (try (Item_Net.update thm)) equations)));
+      (infos, monos, perhaps (try (Item_Net.update (Thm.trim_context thm))) equations)));
 
 
 
@@ -645,7 +653,7 @@
     val ctxt' = Variable.auto_fixes prop ctxt;
     val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of;
     val substs =
-      Item_Net.retrieve (get_equations ctxt) (HOLogic.dest_Trueprop prop)
+      retrieve_equations ctxt (HOLogic.dest_Trueprop prop)
       |> map_filter
         (fn eq => SOME (Pattern.match thy (lhs_of eq, HOLogic.dest_Trueprop prop)
             (Vartab.empty, Vartab.empty), eq)
diff -r 3817a93a3e5e -r 967c16e9c724 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/inductive_set.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -285,9 +285,9 @@
                      warning ("Ignoring conversion rule for operator " ^ s')
                     else (); tab)
                  else
-                   {to_set_simps = thm :: to_set_simps,
+                   {to_set_simps = Thm.trim_context thm :: to_set_simps,
                     to_pred_simps =
-                      mk_to_pred_eq ctxt h fs fs' T' thm :: to_pred_simps,
+                      Thm.trim_context (mk_to_pred_eq ctxt h fs fs' T' thm) :: to_pred_simps,
                     set_arities = Symtab.insert_list op = (s',
                       (T', (map (AList.lookup op = fs) ts', fs'))) set_arities,
                     pred_arities = Symtab.insert_list op = (s,
@@ -347,7 +347,8 @@
     thm |>
     Thm.instantiate ([], insts) |>
     Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimprocs
-      [to_pred_simproc (@{thm mem_Collect_eq} :: @{thm case_prod_conv} :: to_pred_simps)]) |>
+      [to_pred_simproc
+        (@{thm mem_Collect_eq} :: @{thm case_prod_conv} :: map (Thm.transfer thy) to_pred_simps)]) |>
     eta_contract_thm ctxt (is_pred pred_arities) |>
     Rule_Cases.save thm
   end;
diff -r 3817a93a3e5e -r 967c16e9c724 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/HOL/Tools/lin_arith.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -85,8 +85,12 @@
 
 val get_arith_data = Lin_Arith_Data.get o Context.Proof;
 
+fun get_splits ctxt =
+  #splits (get_arith_data ctxt)
+  |> map (Thm.transfer (Proof_Context.theory_of ctxt));
+
 fun add_split thm = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
-  {splits = update Thm.eq_thm_prop thm splits,
+  {splits = update Thm.eq_thm_prop (Thm.trim_context thm) splits,
    inj_consts = inj_consts, discrete = discrete});
 
 fun add_discrete_type d = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
@@ -418,7 +422,7 @@
   (* where ti' = HOLogic.dest_Trueprop ti                                    *)
   fun REPEAT_DETERM_etac_rev_mp tms =
     fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop tms) \<^term>\<open>False\<close>
-  val split_thms  = filter (is_split_thm ctxt) (#splits (get_arith_data ctxt))
+  val split_thms  = filter (is_split_thm ctxt) (get_splits ctxt)
   val cmap        = Splitter.cmap_of_split_thms split_thms
   val goal_tm     = REPEAT_DETERM_etac_rev_mp terms
   val splits      = Splitter.split_posns cmap thy Ts goal_tm
@@ -819,7 +823,7 @@
 
 fun pre_tac ctxt i =
   let
-    val split_thms = filter (is_split_thm ctxt) (#splits (get_arith_data ctxt))
+    val split_thms = filter (is_split_thm ctxt) (get_splits ctxt)
     fun is_relevant t = is_some (decomp ctxt t)
   in
     DETERM (
@@ -940,7 +944,7 @@
     (* split_limit may trigger.                                           *)
     (* Therefore splitting outside of simple_tac may allow us to prove    *)
     (* some goals that simple_tac alone would fail on.                    *)
-    (REPEAT_DETERM o split_tac ctxt (#splits (get_arith_data ctxt)))
+    (REPEAT_DETERM o split_tac ctxt (get_splits ctxt))
     (Fast_Arith.lin_arith_tac ctxt);
 
 in
diff -r 3817a93a3e5e -r 967c16e9c724 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/Isar/attrib.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -29,6 +29,7 @@
     (('c * 'a list) * ('b * 'a list) list) list ->
     (('c * 'att list) * ('fact * 'att list) list) list
   type thms = (thm list * Token.src list) list
+  val trim_context: thms -> thms
   val global_notes: string -> (Attrib.binding * thms) list ->
     theory -> (string * thm list) list * theory
   val local_notes: string -> (Attrib.binding * thms) list ->
@@ -181,6 +182,8 @@
 
 type thms = (thm list * Token.src list) list;
 
+val trim_context: thms -> thms = (map o apfst o map) Thm.trim_context;
+
 fun global_notes kind facts thy = thy |>
   Global_Theory.note_thmss kind (map_facts (map (attribute_global thy)) facts);
 
diff -r 3817a93a3e5e -r 967c16e9c724 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/Isar/bundle.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -55,9 +55,10 @@
 val get_bundle = get_bundle_generic o Context.Proof;
 fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt;
 
-fun define_bundle def context =
+fun define_bundle (b, bundle) context =
   let
-    val (name, bundles') = Name_Space.define context true def (get_bundles_generic context);
+    val bundle' = Attrib.trim_context bundle;
+    val (name, bundles') = Name_Space.define context true (b, bundle') (get_bundles_generic context);
     val context' = (Data.map o apfst o K) bundles' context;
   in (name, context') end;
 
@@ -70,7 +71,7 @@
   | NONE => error "Missing bundle target");
 
 val reset_target = (Context.theory_map o Data.map o apsnd o K) NONE;
-val set_target = Context.theory_map o Data.map o apsnd o K o SOME;
+val set_target = Context.theory_map o Data.map o apsnd o K o SOME o Attrib.trim_context;
 
 fun augment_target thms =
   Local_Theory.background_theory (fn thy => set_target (the_target thy @ thms) thy);
diff -r 3817a93a3e5e -r 967c16e9c724 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/Isar/calculation.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -98,8 +98,11 @@
 
 (* add/del rules *)
 
-val trans_add = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.update);
-val trans_del = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.remove);
+val trans_add =
+  Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.update o Thm.trim_context);
+
+val trans_del =
+  Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.remove);
 
 val sym_add =
   Thm.declaration_attribute (fn th =>
@@ -108,7 +111,7 @@
 
 val sym_del =
   Thm.declaration_attribute (fn th =>
-    (Data.map o apfst o apsnd) (Thm.del_thm (Thm.trim_context th)) #>
+    (Data.map o apfst o apsnd) (Thm.del_thm th) #>
     Thm.attribute_declaration Context_Rules.rule_del th);
 
 
diff -r 3817a93a3e5e -r 967c16e9c724 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/Isar/class.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -87,10 +87,12 @@
   Class_Data {consts = consts, base_sort = base_sort,
     base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
     of_class = of_class, axiom = axiom, defs = defs, operations = operations};
+
 fun map_class_data f (Class_Data {consts, base_sort, base_morph, export_morph, assm_intro,
     of_class, axiom, defs, operations}) =
   make_class_data (f ((consts, base_sort, base_morph, export_morph, assm_intro, of_class, axiom),
     (defs, operations)));
+
 fun merge_class_data _ (Class_Data {consts = consts,
     base_sort = base_sort, base_morph = base_morph, export_morph = export_morph, assm_intro = assm_intro,
     of_class = of_class, axiom = axiom, defs = defs1, operations = operations1},
diff -r 3817a93a3e5e -r 967c16e9c724 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/Isar/context_rules.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -193,7 +193,7 @@
 (* add and del rules *)
 
 
-val rule_del = Thm.declaration_attribute (fn th => Rules.map (del_rule th));
+val rule_del = Thm.declaration_attribute (Rules.map o del_rule);
 
 fun rule_add k view opt_w =
   Thm.declaration_attribute (fn th => Rules.map (add_rule k opt_w (view th) o del_rule th));
diff -r 3817a93a3e5e -r 967c16e9c724 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/Isar/local_defs.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -189,7 +189,7 @@
     (map (Thm.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt))));
 
 val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm o Thm.trim_context);
-val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm o Thm.trim_context);
+val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);
 
 
 (* meta rewrite rules *)
diff -r 3817a93a3e5e -r 967c16e9c724 src/Pure/ML/ml_heap.ML
--- a/src/Pure/ML/ml_heap.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/ML/ml_heap.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -7,6 +7,7 @@
 signature ML_HEAP =
 sig
   val obj_size: 'a -> int
+  val full_gc: unit -> unit
   val share_common_data: unit -> unit
   val save_child: string -> unit
 end;
@@ -16,6 +17,8 @@
 
 val obj_size = PolyML.objSize;
 
+val full_gc = PolyML.fullGC;
+
 fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
 
 fun save_child name =
diff -r 3817a93a3e5e -r 967c16e9c724 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/axclass.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -152,7 +152,11 @@
 
 fun get_info thy c =
   (case Symtab.lookup (axclasses_of thy) c of
-    SOME info => info
+    SOME {def, intro, axioms, params} =>
+      {def = Thm.transfer thy def,
+       intro = Thm.transfer thy intro,
+       axioms = map (Thm.transfer thy) axioms,
+       params = params}
   | NONE => error ("No such axclass: " ^ quote c));
 
 fun all_params_of thy S =
@@ -170,8 +174,6 @@
 fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a;
 
 
-val update_classrel = map_proven_classrels o Symreltab.update;
-
 val is_classrel = Symreltab.defined o proven_classrels_of;
 
 fun the_classrel thy (c1, c2) =
@@ -189,10 +191,11 @@
           else
             (false,
               thy2
-              |> update_classrel ((c1, c2),
+              |> (map_proven_classrels o Symreltab.update) ((c1, c2),
                 (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
                 |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
-                |> Thm.close_derivation));
+                |> Thm.close_derivation
+                |> Thm.trim_context));
 
         val proven = is_classrel thy1;
         val preds = Graph.Keys.fold (fn c1 => proven (c1, c) ? cons c1) all_preds [];
@@ -235,7 +238,8 @@
         val th1 =
           (th RS the_classrel thy (c, c1))
           |> Thm.instantiate' std_vars []
-          |> Thm.close_derivation;
+          |> Thm.close_derivation
+          |> Thm.trim_context;
       in ((th1, thy_name), c1) end);
 
     val finished' = finished andalso null completions;
@@ -243,7 +247,7 @@
   in (finished', arities') end;
 
 fun put_arity_completion ((t, Ss, c), th) thy =
-  let val ar = ((c, Ss), (th, Context.theory_name thy)) in
+  let val ar = ((c, Ss), (Thm.trim_context th, Context.theory_name thy)) in
     thy
     |> map_proven_arities
       (Symtab.insert_list (eq_fst op =) (t, ar) #>
@@ -274,12 +278,13 @@
 
 fun get_inst_param thy (c, tyco) =
   (case Symtab.lookup (the_default Symtab.empty (Symtab.lookup (#1 (inst_params_of thy)) c)) tyco of
-    SOME c' => c'
+    SOME (a, th) => (a, Thm.transfer thy th)
   | NONE => error ("No instance parameter for constant " ^ quote c ^ " on type " ^ quote tyco));
 
-fun add_inst_param (c, tyco) inst =
-  (map_inst_params o apfst o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
-  #> (map_inst_params o apsnd) (Symtab.update_new (#1 inst, (c, tyco)));
+fun add_inst_param (c, tyco) (a, th) =
+  (map_inst_params o apfst o Symtab.map_default (c, Symtab.empty))
+    (Symtab.update_new (tyco, (a, Thm.trim_context th)))
+  #> (map_inst_params o apsnd) (Symtab.update_new (a, (c, tyco)));
 
 val inst_of_param = Symtab.lookup o #2 o inst_params_of;
 val param_of_inst = #1 oo get_inst_param;
@@ -392,7 +397,8 @@
     val (th', thy') = Global_Theory.store_thm (binding, th) thy;
     val th'' = th'
       |> Thm.unconstrainT
-      |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
+      |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy' (TVar ((Name.aT, 0), [])))] []
+      |> Thm.trim_context;
   in
     thy'
     |> Sign.primitive_classrel (c1, c2)
@@ -414,7 +420,7 @@
 
     val args = Name.invent_names Name.context Name.aT Ss;
     val T = Type (t, map TFree args);
-    val std_vars = map (fn (a, S) => SOME (Thm.global_ctyp_of thy' (TVar ((a, 0), [])))) args;
+    val std_vars = map (fn (a, _) => SOME (Thm.global_ctyp_of thy' (TVar ((a, 0), [])))) args;
 
     val missing_params = Sign.complete_sort thy' [c]
       |> maps (these o Option.map #params o try (get_info thy'))
@@ -450,7 +456,6 @@
   let
     val ctxt = Proof_Context.init_global thy;
     val arity = Proof_Context.cert_arity ctxt raw_arity;
-    val names = map (prefix arity_prefix) (Logic.name_arities arity);
     val props = Logic.mk_arities arity;
     val ths =
       Goal.prove_common ctxt NONE [] [] props
@@ -556,11 +561,14 @@
 
     (* result *)
 
-    val axclass = make_axclass (def, intro, axioms, params);
+    val axclass =
+      make_axclass
+        (Thm.trim_context def, Thm.trim_context intro, map Thm.trim_context axioms, params);
     val result_thy =
       facts_thy
       |> map_proven_classrels
-          (fold2 (fn c => fn th => Symreltab.update ((class, c), th)) super classrel)
+          (fold2 (fn c => fn th => Symreltab.update ((class, c), Thm.trim_context th))
+            super classrel)
       |> perhaps complete_classrels
       |> Sign.qualified_path false bconst
       |> Global_Theory.note_thmss "" (name_atts ~~ map Thm.simple_fact (unflat axiomss axioms))
@@ -589,9 +597,6 @@
     |-> fold (add o Drule.export_without_context o snd)
   end;
 
-fun class_const c =
-  (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
-
 fun class_const_dep c =
   ((Defs.Const, Logic.const_of_class c), [Term.aT []]);
 
diff -r 3817a93a3e5e -r 967c16e9c724 src/Pure/context.ML
--- a/src/Pure/context.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Pure/context.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -48,8 +48,11 @@
   val proper_subthy: theory * theory -> bool
   val subthy_id: theory_id * theory_id -> bool
   val subthy: theory * theory -> bool
+  val trace_theories: bool Unsynchronized.ref
+  val theories_trace: unit -> {active: int, all: int}
+  val begin_thy: string -> theory list -> theory
   val finish_thy: theory -> theory
-  val begin_thy: string -> theory list -> theory
+  val theory_data_size: theory -> (Position.T * int) list
   (*proof context*)
   val raw_transfer: theory -> Proof.context -> Proof.context
   (*certificate*)
@@ -125,7 +128,9 @@
 
 datatype theory =
   Theory of
-   theory_id *
+   (*identity*)
+   {theory_id: theory_id,
+    token: unit Unsynchronized.ref} *
    (*ancestry*)
    {parents: theory list,         (*immediate predecessors*)
     ancestors: theory list} *     (*all predecessors -- canonical reverse order*)
@@ -137,7 +142,8 @@
 fun rep_theory_id (Theory_Id args) = args;
 fun rep_theory (Theory args) = args;
 
-val theory_id = #1 o rep_theory;
+val theory_identity = #1 o rep_theory;
+val theory_id = #theory_id o theory_identity;
 
 val identity_of_id = #1 o rep_theory_id;
 val identity_of = identity_of_id o theory_id;
@@ -202,12 +208,12 @@
 
 fun insert_id id ids = Inttab.update (id, ()) ids;
 
-fun merge_ids
-    (Theory (Theory_Id ({id = id1, ids = ids1, ...}, _), _, _))
-    (Theory (Theory_Id ({id = id2, ids = ids2, ...}, _), _, _)) =
-  Inttab.merge (K true) (ids1, ids2)
-  |> insert_id id1
-  |> insert_id id2;
+val merge_ids =
+  apply2 theory_id #>
+  (fn (Theory_Id ({id = id1, ids = ids1, ...}, _), Theory_Id ({id = id2, ids = ids2, ...}, _)) =>
+    Inttab.merge (K true) (ids1, ids2)
+    |> insert_id id1
+    |> insert_id id2);
 
 
 (* equality and inclusion *)
@@ -265,6 +271,7 @@
 
 in
 
+fun invoke_pos k = invoke "" (K o #pos) k ();
 fun invoke_empty k = invoke "" (K o #empty) k ();
 val invoke_extend = invoke "extend" #extend;
 fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys);
@@ -285,10 +292,44 @@
 
 (** build theories **)
 
-(* primitives *)
+(* create theory *)
+
+val trace_theories = Unsynchronized.ref false;
+
+local
+
+val theories =
+  Synchronized.var "theory_tokens" ([]: unit Unsynchronized.ref option Unsynchronized.ref list);
+
+val dummy_token = Unsynchronized.ref ();
+
+fun make_token () =
+  if ! trace_theories then
+    let
+      val token = Unsynchronized.ref ();
+      val _ = Synchronized.change theories (cons (Weak.weak (SOME token)));
+    in token end
+  else dummy_token;
+
+in
+
+fun theories_trace () =
+  let
+    val trace = Synchronized.value theories;
+    val _ = ML_Heap.full_gc ();
+    val active = fold (fn Unsynchronized.ref NONE => I | _ => Integer.add 1) trace 0;
+  in {all = length trace, active = active} end;
 
 fun create_thy ids history ancestry data =
-  Theory (Theory_Id (make_identity (serial ()) ids, history), ancestry, data);
+  let
+    val theory_id = Theory_Id (make_identity (serial ()) ids, history);
+    val token = make_token ();
+  in Theory ({theory_id = theory_id, token = token}, ancestry, data) end;
+
+end;
+
+
+(* primitives *)
 
 val pre_pure_thy =
   create_thy Inttab.empty (make_history PureN 0) (make_ancestry [] []) Datatab.empty;
@@ -297,7 +338,8 @@
 
 fun change_thy finish f thy =
   let
-    val Theory (Theory_Id ({id, ids}, {name, stage}), ancestry, data) = thy;
+    val Theory_Id ({id, ids}, {name, stage}) = theory_id thy;
+    val Theory (_, ancestry, data) = thy;
     val (ancestry', data') =
       if stage = finished then
         (make_ancestry [thy] (extend_ancestors thy (ancestors_of thy)), extend_data data)
@@ -320,12 +362,12 @@
 
 local
 
-fun merge_thys (thy1, thy2) =
+fun merge_thys thys =
   let
-    val ids = merge_ids thy1 thy2;
+    val ids = merge_ids thys;
     val history = make_history "" 0;
     val ancestry = make_ancestry [] [];
-    val data = merge_data (thy1, thy2) (data_of thy1, data_of thy2);
+    val data = merge_data thys (apply2 data_of thys);
   in create_thy ids history ancestry data end;
 
 fun maximal_thys thys =
@@ -342,15 +384,16 @@
         Library.foldl merge_ancestors ([], map ancestors_of parents)
         |> fold extend_ancestors parents;
 
-      val Theory (Theory_Id ({ids, ...}, _), _, data) =
+      val thy0 =
         (case parents of
           [] => error "Missing theory imports"
         | [thy] => extend_thy thy
         | thy :: thys => Library.foldl merge_thys (thy, thys));
+      val Theory_Id ({ids, ...}, _) = theory_id thy0;
 
       val history = make_history name 0;
       val ancestry = make_ancestry parents ancestors;
-    in create_thy ids history ancestry data end;
+    in create_thy ids history ancestry (data_of thy0) end;
 
 end;
 
@@ -369,8 +412,17 @@
 
 fun put k mk x = update_thy (Datatab.update (k, mk x));
 
+fun obj_size k thy =
+  Datatab.lookup (data_of thy) k |> Option.map ML_Heap.obj_size;
+
 end;
 
+fun theory_data_size thy =
+  (data_of thy, []) |-> Datatab.fold_rev (fn (k, _) =>
+    (case Theory_Data.obj_size k thy of
+      NONE => I
+    | SOME n => (cons (invoke_pos k, n))));
+
 
 
 (*** proof context ***)
diff -r 3817a93a3e5e -r 967c16e9c724 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Sat Feb 03 09:11:21 2018 +0000
+++ b/src/Tools/Code/code_runtime.ML	Sat Feb 17 11:11:28 2018 +0100
@@ -349,10 +349,12 @@
     val thms = Simplifier.mksimps (Proof_Context.init_global thy) thm;
   in
     thy
-    |> Computation_Preproc_Data.map (union Thm.eq_thm_prop thms)
+    |> Computation_Preproc_Data.map (fold (insert Thm.eq_thm_prop o Thm.trim_context) thms)
   end;
 
-fun get ctxt = Computation_Preproc_Data.get (Proof_Context.theory_of ctxt);
+fun get ctxt =
+  Computation_Preproc_Data.get (Proof_Context.theory_of ctxt)
+  |> map (Thm.transfer (Proof_Context.theory_of ctxt))
 
 in