# HG changeset patch
# User wenzelm
# Date 1519395471 -3600
# Node ID f7e37a94caee1d60bfaeac81f36b96e24bb261b0
# Parent  4fa9d5ef95bc661c5892cb1728392bef5e7858eb# Parent  23d46836a5acfc1390a2502ec20af0df10a73a76
merged

diff -r 4fa9d5ef95bc -r f7e37a94caee NEWS
--- a/NEWS	Fri Feb 23 10:52:31 2018 +0000
+++ b/NEWS	Fri Feb 23 15:17:51 2018 +0100
@@ -167,6 +167,15 @@
 latex and bibtex process. Minor INCOMPATIBILITY.
 
 
+*** Isar ***
+
+* Command 'interpret' no longer exposes resulting theorems as literal
+facts, notably for the \<open>prop\<close> notation or the "fact" proof method. This
+improves modularity of proofs and scalability of locale interpretation.
+Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
+(e.g. use 'find_theorems' or 'try' to figure this out).
+
+
 *** HOL ***
 
 * Clarifed theorem names:
diff -r 4fa9d5ef95bc -r f7e37a94caee src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 23 10:52:31 2018 +0000
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 23 15:17:51 2018 +0100
@@ -849,10 +849,9 @@
                 |> infer_instantiate' lthy (replicate live NONE @
                   [SOME (Thm.cterm_of lthy (ctorA $ y))])
                 |> unfold_thms lthy [dtor_ctor];
-
-              val map_ctor_thm0 = fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans);
             in
-              Thm.generalize ([], [y_s]) (Thm.maxidx_of map_ctor_thm0 + 1) map_ctor_thm0
+              (fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans))
+              |> Drule.generalize ([], [y_s])
             end;
 
         val map_thms =
@@ -926,13 +925,12 @@
               val ((y as Free (y_s, _), z as Free (z_s, _)), _) = lthy
                 |> yield_singleton (mk_Frees "y") y_T
                 ||>> yield_singleton (mk_Frees "z") z_T;
-
-              val rel_ctor_thm0 = fp_rel_thm
-                |> infer_instantiate' lthy (replicate live NONE @
-                  [SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))])
-                |> unfold_thms lthy [dtor_ctor];
             in
-              Thm.generalize ([], [y_s, z_s]) (Thm.maxidx_of rel_ctor_thm0 + 1) rel_ctor_thm0
+              fp_rel_thm
+              |> infer_instantiate' lthy (replicate live NONE @
+                [SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))])
+              |> unfold_thms lthy [dtor_ctor]
+              |> Drule.generalize ([], [y_s, z_s])
             end;
 
         val rel_inject_thms =
diff -r 4fa9d5ef95bc -r f7e37a94caee src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Fri Feb 23 10:52:31 2018 +0000
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Fri Feb 23 15:17:51 2018 +0100
@@ -158,9 +158,9 @@
     let
       val s = Name.uu;
       val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
-      val split' = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split;
     in
-      Thm.generalize ([], [s]) (Thm.maxidx_of split' + 1) split'
+      Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split
+      |> Drule.generalize ([], [s])
     end
   | _ => split);
 
diff -r 4fa9d5ef95bc -r f7e37a94caee src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Fri Feb 23 10:52:31 2018 +0000
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Fri Feb 23 15:17:51 2018 +0100
@@ -187,7 +187,7 @@
           let
             val [rty, rty'] = binder_types typ
           in
-            if Term.is_TVar rty andalso is_Type rty' then
+            if Term.is_TVar rty andalso Term.is_Type rty' then
               (xi, Thm.cterm_of ctxt (HOLogic.eq_const rty')) :: subst
             else
               subst
@@ -472,7 +472,7 @@
     if same_type_constrs (rty, qty) then
       forall (no_no_code ctxt) (Targs rty ~~ Targs qty)
     else
-      if is_Type qty then
+      if Term.is_Type qty then
         if Lifting_Info.is_no_code_type ctxt (Tname qty) then false
         else
           let
diff -r 4fa9d5ef95bc -r f7e37a94caee src/HOL/Tools/Lifting/lifting_util.ML
--- a/src/HOL/Tools/Lifting/lifting_util.ML	Fri Feb 23 10:52:31 2018 +0000
+++ b/src/HOL/Tools/Lifting/lifting_util.ML	Fri Feb 23 15:17:51 2018 +0100
@@ -25,7 +25,6 @@
   val get_args: int -> term -> term list
   val strip_args: int -> term -> term
   val all_args_conv: conv -> conv
-  val is_Type: typ -> bool
   val same_type_constrs: typ * typ -> bool
   val Targs: typ -> typ list
   val Tname: typ -> string
@@ -108,9 +107,6 @@
 
 fun all_args_conv conv ctm = Conv.try_conv (Conv.combination_conv (all_args_conv conv) conv) ctm
 
-fun is_Type (Type _) = true
-  | is_Type _ = false
-
 fun same_type_constrs (Type (r, _), Type (q, _)) = (r = q)
   | same_type_constrs _ = false
 
diff -r 4fa9d5ef95bc -r f7e37a94caee src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Feb 23 10:52:31 2018 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Feb 23 15:17:51 2018 +0100
@@ -83,7 +83,6 @@
   val const_match : theory -> (string * typ) * (string * typ) -> bool
   val term_match : theory -> term * term -> bool
   val frac_from_term_pair : typ -> term -> term -> term
-  val is_TFree : typ -> bool
   val is_fun_type : typ -> bool
   val is_set_type : typ -> bool
   val is_fun_or_set_type : typ -> bool
@@ -478,9 +477,6 @@
           | n2 => Const (@{const_name divide}, T --> T --> T)
                   $ HOLogic.mk_number T n1 $ HOLogic.mk_number T n2
 
-fun is_TFree (TFree _) = true
-  | is_TFree _ = false
-
 fun is_fun_type (Type (@{type_name fun}, _)) = true
   | is_fun_type _ = false
 
diff -r 4fa9d5ef95bc -r f7e37a94caee src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Fri Feb 23 10:52:31 2018 +0000
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Fri Feb 23 15:17:51 2018 +0100
@@ -38,9 +38,6 @@
 
 fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst
 
-fun is_Type (Type _) = true
-  | is_Type _ = false
-
 fun bnf_only_type_ctr f bnf = if is_Type (T_of_bnf bnf) then f bnf else I
 
 fun bnf_of_fp_sugar (fp_sugar:fp_sugar) = nth (#bnfs (#fp_res fp_sugar)) (#fp_res_index fp_sugar)
diff -r 4fa9d5ef95bc -r f7e37a94caee src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Fri Feb 23 10:52:31 2018 +0000
+++ b/src/Pure/Isar/class_declaration.ML	Fri Feb 23 15:17:51 2018 +0100
@@ -29,15 +29,19 @@
   let
     val empty_ctxt = Proof_Context.init_global thy;
 
+    val certT = Thm.trim_context_ctyp o Thm.global_ctyp_of thy;
+    val cert = Thm.trim_context_cterm o Thm.global_cterm_of thy;
+
     (* instantiation of canonical interpretation *)
-    val aT = TFree (Name.aT, base_sort);
+    val a_tfree = (Name.aT, base_sort);
+    val a_type = TFree a_tfree;
     val param_map_const = (map o apsnd) Const param_map;
-    val param_map_inst = (map o apsnd)
-      (Const o apsnd (map_atyps (K aT))) param_map;
-    val const_morph = Element.inst_morphism thy
-      (Symtab.empty, Symtab.make param_map_inst);
-    val typ_morph = Element.inst_morphism thy
-      (Symtab.empty |> Symtab.update (Name.aT, TFree (Name.aT, [class])), Symtab.empty);
+    val param_map_inst = param_map |> map (fn (x, (c, T)) =>
+      let val T' = map_atyps (K a_type) T in ((x, T'), cert (Const (c, T'))) end);
+    val const_morph =
+      Element.instantiate_normalize_morphism ([], param_map_inst);
+    val typ_morph =
+      Element.instantiate_normalize_morphism ([(a_tfree, certT (TFree (Name.aT, [class])))], [])
     val (([raw_props], _, [(_, raw_inst_morph)], _, export_morph), _) = empty_ctxt
       |> Expression.cert_goal_expression ([(class, (("", false),
            (Expression.Named param_map_const, [])))], []);
@@ -84,16 +88,16 @@
     val some_assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
 
     (* of_class *)
-    val of_class_prop_concl = Logic.mk_of_class (aT, class);
+    val of_class_prop_concl = Logic.mk_of_class (a_type, class);
     val of_class_prop =
       (case some_prop of
         NONE => of_class_prop_concl
       | SOME prop => Logic.mk_implies (Morphism.term const_morph
-          ((map_types o map_atyps) (K aT) prop), of_class_prop_concl));
+          ((map_types o map_atyps) (K a_type) prop), of_class_prop_concl));
     val sup_of_classes = map (snd o Class.rules thy) sups;
     val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
     val axclass_intro = #intro (Axclass.get_info thy class);
-    val base_sort_trivs = Thm.of_sort (Thm.global_ctyp_of thy aT, base_sort);
+    val base_sort_trivs = Thm.of_sort (Thm.global_ctyp_of thy a_type, base_sort);
     fun tac ctxt =
       REPEAT (SOMEGOAL
         (match_tac ctxt (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
diff -r 4fa9d5ef95bc -r f7e37a94caee src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Fri Feb 23 10:52:31 2018 +0000
+++ b/src/Pure/Isar/element.ML	Fri Feb 23 15:17:51 2018 +0100
@@ -47,8 +47,8 @@
   val transform_witness: morphism -> witness -> witness
   val conclude_witness: Proof.context -> witness -> thm
   val pretty_witness: Proof.context -> witness -> Pretty.T
-  val instT_morphism: theory -> typ Symtab.table -> morphism
-  val inst_morphism: theory -> typ Symtab.table * term Symtab.table -> morphism
+  val instantiate_normalize_morphism:
+    ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> morphism
   val satisfy_morphism: witness list -> morphism
   val eq_morphism: theory -> thm list -> morphism option
   val init: context_i -> Context.generic -> Context.generic
@@ -321,18 +321,6 @@
 
 end;
 
-
-fun compose_witness (Witness (_, th)) r =
-  let
-    val th' = Goal.conclude th;
-    val A = Thm.cprem_of r 1;
-  in
-    Thm.implies_elim
-      (Conv.gconv_rule Drule.beta_eta_conversion 1 r)
-      (Conv.fconv_rule Drule.beta_eta_conversion
-        (Thm.instantiate (Thm.match (Thm.cprop_of th', A)) th'))
-  end;
-
 fun conclude_witness ctxt (Witness (_, th)) =
   Thm.close_derivation (Raw_Simplifier.norm_hhf_protect ctxt (Goal.conclude th));
 
@@ -344,127 +332,52 @@
   end;
 
 
-(* derived rules *)
-
-fun instantiate_tfrees thy subst th =
-  let
-    val idx = Thm.maxidx_of th + 1;
-    fun cert_inst (a, (S, T)) = (((a, idx), S), Thm.global_ctyp_of thy T);
-
-    fun add_inst (a, S) insts =
-      if AList.defined (op =) insts a then insts
-      else (case AList.lookup (op =) subst a of NONE => insts | SOME T => (a, (S, T)) :: insts);
-    val insts =
-      (Term.fold_types o Term.fold_atyps) (fn TFree v => add_inst v | _ => I)
-        (Thm.full_prop_of th) [];
-  in
-    th
-    |> Thm.generalize (map fst insts, []) idx
-    |> Thm.instantiate (map cert_inst insts, [])
-  end;
-
-fun instantiate_frees thy subst =
-  Drule.forall_intr_list (map (Thm.global_cterm_of thy o Free o fst) subst) #>
-  Drule.forall_elim_list (map (Thm.global_cterm_of thy o snd) subst);
-
-fun hyps_rule rule th =
-  let val hyps = Thm.chyps_of th in
-    Drule.implies_elim_list
-      (rule (Drule.implies_intr_list hyps th))
-      (map (Thm.assume o Drule.cterm_rule rule) hyps)
-  end;
-
-
-(* instantiate types *)
-
-fun instT_type_same env =
-  if Symtab.is_empty env then Same.same
-  else
-    Term_Subst.map_atypsT_same
-      (fn TFree (a, _) => (case Symtab.lookup env a of SOME T => T | NONE => raise Same.SAME)
-        | _ => raise Same.SAME);
-
-fun instT_term_same env =
-  if Symtab.is_empty env then Same.same
-  else Term_Subst.map_types_same (instT_type_same env);
-
-val instT_type = Same.commit o instT_type_same;
-val instT_term = Same.commit o instT_term_same;
-
-fun instT_subst env th =
-  (Thm.fold_terms o Term.fold_types o Term.fold_atyps)
-    (fn T as TFree (a, _) =>
-      let val T' = the_default T (Symtab.lookup env a)
-      in if T = T' then I else insert (eq_fst (op =)) (a, T') end
-    | _ => I) th [];
+(* instantiate frees, with beta normalization *)
 
-fun instT_thm thy env th =
-  if Symtab.is_empty env then th
-  else
-    let val subst = instT_subst env th
-    in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end;
-
-fun instT_morphism thy env =
-  Morphism.morphism "Element.instT"
-   {binding = [],
-    typ = [instT_type env],
-    term = [instT_term env],
-    fact = [map (instT_thm thy env)]};
-
-
-(* instantiate types and terms *)
-
-fun inst_term (envT, env) =
-  if Symtab.is_empty env then instT_term envT
-  else
-    instT_term envT #>
-    Same.commit (Term_Subst.map_aterms_same
-      (fn Free (x, _) => (case Symtab.lookup env x of SOME t => t | NONE => raise Same.SAME)
-        | _ => raise Same.SAME)) #>
-    Envir.beta_norm;
-
-fun inst_subst (envT, env) th =
-  (Thm.fold_terms o Term.fold_aterms)
-    (fn Free (x, T) =>
-      let
-        val T' = instT_type envT T;
-        val t = Free (x, T');
-        val t' = the_default t (Symtab.lookup env x);
-      in if t aconv t' then I else insert (eq_fst (op =)) ((x, T'), t') end
-    | _ => I) th [];
-
-fun inst_thm thy (envT, env) th =
-  if Symtab.is_empty env then instT_thm thy envT th
-  else
-    let
-      val substT = instT_subst envT th;
-      val subst = inst_subst (envT, env) th;
-    in
-      if null substT andalso null subst then th
-      else th |> hyps_rule
-       (instantiate_tfrees thy substT #>
-        instantiate_frees thy subst #>
-        Conv.fconv_rule (Thm.beta_conversion true))
-    end;
-
-fun inst_morphism thy (envT, env) =
-  Morphism.morphism "Element.inst"
-   {binding = [],
-    typ = [instT_type envT],
-    term = [inst_term (envT, env)],
-    fact = [map (inst_thm thy (envT, env))]};
+fun instantiate_normalize_morphism insts =
+  Morphism.instantiate_frees_morphism insts $>
+  Morphism.term_morphism "beta_norm" Envir.beta_norm $>
+  Morphism.thm_morphism "beta_conversion" (Conv.fconv_rule (Thm.beta_conversion true));
 
 
 (* satisfy hypotheses *)
 
+local
+
+val norm_term = Envir.beta_eta_contract;
+val norm_conv = Drule.beta_eta_conversion;
+val norm_cterm = Thm.rhs_of o norm_conv;
+
+fun find_witness witns hyp =
+  (case find_first (fn Witness (t, _) => hyp aconv t) witns of
+    NONE =>
+      let val hyp' = norm_term hyp
+      in find_first (fn Witness (t, _) => hyp' aconv norm_term t) witns end
+  | some => some);
+
+fun compose_witness (Witness (_, th)) r =
+  let
+    val th' = Goal.conclude th;
+    val A = Thm.cprem_of r 1;
+  in
+    Thm.implies_elim
+      (Conv.gconv_rule norm_conv 1 r)
+      (Conv.fconv_rule norm_conv
+        (Thm.instantiate (Thm.match (apply2 norm_cterm (Thm.cprop_of th', A))) th'))
+  end;
+
+in
+
 fun satisfy_thm witns thm =
-  thm |> fold (fn hyp =>
-    (case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of
+  (Thm.chyps_of thm, thm) |-> fold (fn hyp =>
+    (case find_witness witns (Thm.term_of hyp) of
       NONE => I
-    | SOME w => Thm.implies_intr hyp #> compose_witness w)) (Thm.chyps_of thm);
+    | SOME w => Thm.implies_intr hyp #> compose_witness w));
 
 val satisfy_morphism = Morphism.thm_morphism "Element.satisfy" o satisfy_thm;
 
+end;
+
 
 (* rewriting with equalities *)
 
diff -r 4fa9d5ef95bc -r f7e37a94caee src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Feb 23 10:52:31 2018 +0000
+++ b/src/Pure/Isar/expression.ML	Fri Feb 23 15:17:51 2018 +0100
@@ -169,24 +169,30 @@
 fun inst_morphism (parm_names, parm_types) ((prfx, mandatory), insts') ctxt =
   let
     (* parameters *)
-    val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
+    val type_parms = fold Term.add_tfreesT parm_types [];
 
-    (* type inference and contexts *)
+    (* type inference *)
     val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
-    val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
-    val arg = type_parms @ map2 Type.constraint parm_types' insts';
-    val res = Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt) arg;
-    val ctxt' = ctxt |> fold Variable.auto_fixes res;
+    val type_parms' = fold Term.add_tvarsT parm_types' [];
+    val checked =
+      (map (Logic.mk_type o TVar) type_parms' @ map2 Type.constraint parm_types' insts')
+      |> Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt)
+    val (type_parms'', insts'') = chop (length type_parms') checked;
+
+    (* context *)
+    val ctxt' = fold Variable.auto_fixes checked ctxt;
+    val certT = Thm.trim_context_ctyp o Thm.ctyp_of ctxt';
+    val cert = Thm.trim_context_cterm o Thm.cterm_of ctxt';
 
     (* instantiation *)
-    val (type_parms'', res') = chop (length type_parms) res;
-    val insts'' = (parm_names ~~ res') |> map_filter
-      (fn inst as (x, Free (y, _)) => if x = y then NONE else SOME inst
-        | inst => SOME inst);
-    val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
-    val inst = Symtab.make insts'';
+    val instT =
+      (type_parms ~~ map Logic.dest_type type_parms'')
+      |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T));
+    val cert_inst =
+      ((parm_names ~~ map (Term_Subst.instantiateT_frees instT) parm_types) ~~ insts'')
+      |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t));
   in
-    (Element.inst_morphism (Proof_Context.theory_of ctxt) (instT, inst) $>
+    (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $>
       Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt')
   end;
 
@@ -309,8 +315,7 @@
 fun finish_inst ctxt (loc, (prfx, inst)) =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
-    val (morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst) ctxt;
+    val (morph, _) = inst_morphism (Locale.params_types_of thy loc) (prfx, inst) ctxt;
   in (loc, morph) end;
 
 fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) =>
@@ -371,23 +376,26 @@
 
     fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) =
       let
-        val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
+        val (parm_names, parm_types) = Locale.params_types_of thy loc;
         val inst' = prep_inst ctxt parm_names inst;
         val eqns' = map (apsnd (parse_eqn ctxt)) eqns;
         val parm_types' = parm_types
-          |> map (Type_Infer.paramify_vars o
-              Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global);
+          |> map (Logic.varifyT_global #>
+              Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) #>
+              Type_Infer.paramify_vars);
         val inst'' = map2 Type.constraint parm_types' inst';
         val insts' = insts @ [(loc, (prfx, inst''))];
         val eqnss' = eqnss @ [eqns'];
         val ((insts'', eqnss'', _, _), _) = check_autofix insts' eqnss' [] [] ctxt;
-        val inst''' = insts'' |> List.last |> snd |> snd;
-        val eqns'' = eqnss'' |> List.last;
-        val (inst_morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst''') ctxt;
-        val rewrite_morph = eqns'' |> map (snd #> Thm.cterm_of ctxt #> Thm.assume #> Local_Defs.abs_def_rule ctxt) |>
-           Element.eq_morphism (Proof_Context.theory_of ctxt) |> the_default Morphism.identity;
-        val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
-      in (i + 1, insts', eqnss', ctxt'') end;
+        val (inst_morph, _) =
+          inst_morphism (parm_names, parm_types) (prfx, #2 (#2 (List.last insts''))) ctxt;
+        val rewrite_morph =
+          List.last eqnss''
+          |> map (snd #> Thm.cterm_of ctxt #> Thm.assume #> Local_Defs.abs_def_rule ctxt)
+          |> Element.eq_morphism (Proof_Context.theory_of ctxt)
+          |> the_default Morphism.identity;
+        val ctxt' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
+      in (i + 1, insts', eqnss', ctxt') end;
 
     fun prep_elem raw_elem ctxt =
       let
diff -r 4fa9d5ef95bc -r f7e37a94caee src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Fri Feb 23 10:52:31 2018 +0000
+++ b/src/Pure/Isar/interpretation.ML	Fri Feb 23 15:17:51 2018 +0100
@@ -175,10 +175,14 @@
     fun setup_proof after_qed propss eqns goal_ctxt =
       Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
         propss eqns goal_ctxt state;
+    fun add_registration reg mixin export ctxt = ctxt
+      |> Proof_Context.set_stmt false
+      |> Context.proof_map (Locale.add_registration reg mixin export)
+      |> Proof_Context.restore_stmt ctxt;
   in
     Proof.context_of state
     |> generic_interpretation prep_interpretation setup_proof
-      Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression [] raw_eqns
+      Attrib.local_notes add_registration expression [] raw_eqns
   end;
 
 in
diff -r 4fa9d5ef95bc -r f7e37a94caee src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Feb 23 10:52:31 2018 +0000
+++ b/src/Pure/Isar/locale.ML	Fri Feb 23 15:17:51 2018 +0100
@@ -49,6 +49,7 @@
   val pretty_name: Proof.context -> string -> Pretty.T
   val defined: theory -> string -> bool
   val params_of: theory -> string -> ((string * typ) * mixfix) list
+  val params_types_of: theory -> string -> string list * typ list
   val intros_of: theory -> string -> thm option * thm option
   val axioms_of: theory -> string -> thm list
   val instance_of: theory -> string -> morphism -> term list
@@ -212,6 +213,7 @@
 (** Primitive operations **)
 
 fun params_of thy = snd o #parameters o the_locale thy;
+fun params_types_of thy loc = split_list (map #1 (params_of thy loc));
 
 fun intros_of thy = (apply2 o Option.map) (Thm.transfer thy) o #intros o the_locale thy;
 
diff -r 4fa9d5ef95bc -r f7e37a94caee src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Fri Feb 23 10:52:31 2018 +0000
+++ b/src/Pure/Syntax/printer.ML	Fri Feb 23 15:17:51 2018 +0100
@@ -75,7 +75,7 @@
 fun type_emphasis ctxt T =
   T <> dummyT andalso
     (Config.get ctxt show_types orelse Config.get ctxt show_markup orelse
-      Config.get ctxt show_type_emphasis andalso not (can dest_Type T));
+      Config.get ctxt show_type_emphasis andalso not (is_Type T));
 
 
 
diff -r 4fa9d5ef95bc -r f7e37a94caee src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Fri Feb 23 10:52:31 2018 +0000
+++ b/src/Pure/more_thm.ML	Fri Feb 23 15:17:51 2018 +0100
@@ -72,6 +72,7 @@
   val forall_intr_name: string * cterm -> thm -> thm
   val forall_elim_var: int -> thm -> thm
   val forall_elim_vars: int -> thm -> thm
+  val instantiate_frees: ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> thm -> thm
   val instantiate': ctyp option list -> cterm option list -> thm -> thm
   val forall_intr_frees: thm -> thm
   val unvarify_global: theory -> thm -> thm
@@ -406,6 +407,29 @@
 end;
 
 
+(* instantiate frees *)
+
+fun instantiate_frees ([], []) th = th
+  | instantiate_frees (instT, inst) th =
+      let
+        val idx = Thm.maxidx_of th + 1;
+        fun index ((a, A), b) = (((a, idx), A), b);
+        val insts = (map index instT, map index inst);
+        val frees = (map (#1 o #1) instT, map (#1 o #1) inst);
+
+        val hyps = Thm.chyps_of th;
+        val inst_cterm =
+          Thm.generalize_cterm frees idx #>
+          Thm.instantiate_cterm insts;
+      in
+        th
+        |> fold_rev Thm.implies_intr hyps
+        |> Thm.generalize frees idx
+        |> Thm.instantiate insts
+        |> fold (elim_implies o Thm.assume o inst_cterm) hyps
+      end;
+
+
 (* instantiate by left-to-right occurrence of variables *)
 
 fun instantiate' cTs cts thm =
diff -r 4fa9d5ef95bc -r f7e37a94caee src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Fri Feb 23 10:52:31 2018 +0000
+++ b/src/Pure/morphism.ML	Fri Feb 23 15:17:51 2018 +0100
@@ -42,6 +42,8 @@
   val transfer_morphism': Proof.context -> morphism
   val transfer_morphism'': Context.generic -> morphism
   val trim_context_morphism: morphism
+  val instantiate_frees_morphism:
+    ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> morphism
   val instantiate_morphism:
     ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> morphism
 end;
@@ -127,6 +129,22 @@
 
 val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context;
 
+
+(* instantiate *)
+
+fun instantiate_frees_morphism ([], []) = identity
+  | instantiate_frees_morphism (cinstT, cinst) =
+      let
+        val instT = map (apsnd Thm.typ_of) cinstT;
+        val inst = map (apsnd Thm.term_of) cinst;
+      in
+        morphism "instantiate_frees"
+          {binding = [],
+           typ = if null instT then [] else [Term_Subst.instantiateT_frees instT],
+           term = [Term_Subst.instantiate_frees (instT, inst)],
+           fact = [map (Thm.instantiate_frees (cinstT, cinst))]}
+      end;
+
 fun instantiate_morphism ([], []) = identity
   | instantiate_morphism (cinstT, cinst) =
       let
diff -r 4fa9d5ef95bc -r f7e37a94caee src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Feb 23 10:52:31 2018 +0000
+++ b/src/Pure/term.ML	Fri Feb 23 15:17:51 2018 +0100
@@ -34,14 +34,16 @@
   val no_dummyT: typ -> typ
   val --> : typ * typ -> typ
   val ---> : typ list * typ -> typ
+  val is_Type: typ -> bool
+  val is_TFree: typ -> bool
+  val is_TVar: typ -> bool
   val dest_Type: typ -> string * typ list
+  val dest_TFree: typ -> string * sort
   val dest_TVar: typ -> indexname * sort
-  val dest_TFree: typ -> string * sort
   val is_Bound: term -> bool
   val is_Const: term -> bool
   val is_Free: term -> bool
   val is_Var: term -> bool
-  val is_TVar: typ -> bool
   val dest_Const: term -> string * typ
   val dest_Free: term -> string * typ
   val dest_Var: term -> indexname * typ
@@ -246,12 +248,29 @@
 (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
 val op ---> = Library.foldr (op -->);
 
+
+(** Discriminators **)
+
+fun is_Type (Type _) = true
+  | is_Type _ = false;
+
+fun is_TFree (TFree _) = true
+  | is_TFree _ = false;
+
+fun is_TVar (TVar _) = true
+  | is_TVar _ = false;
+
+
+(** Destructors **)
+
 fun dest_Type (Type x) = x
   | dest_Type T = raise TYPE ("dest_Type", [T], []);
+
+fun dest_TFree (TFree x) = x
+  | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
+
 fun dest_TVar (TVar x) = x
   | dest_TVar T = raise TYPE ("dest_TVar", [T], []);
-fun dest_TFree (TFree x) = x
-  | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
 
 
 (** Discriminators **)
@@ -268,9 +287,6 @@
 fun is_Var (Var _) = true
   | is_Var _ = false;
 
-fun is_TVar (TVar _) = true
-  | is_TVar _ = false;
-
 
 (** Destructors **)
 
diff -r 4fa9d5ef95bc -r f7e37a94caee src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Fri Feb 23 10:52:31 2018 +0000
+++ b/src/Pure/term_subst.ML	Fri Feb 23 15:17:51 2018 +0100
@@ -17,6 +17,12 @@
   val instantiate_maxidx:
     ((indexname * sort) * (typ * int)) list * ((indexname * typ) * (term * int)) list ->
     term -> int -> term * int
+  val instantiateT_frees_same: ((string * sort) * typ) list -> typ Same.operation
+  val instantiate_frees_same: ((string * sort) * typ) list * ((string * typ) * term) list ->
+    term Same.operation
+  val instantiateT_frees: ((string * sort) * typ) list -> typ -> typ
+  val instantiate_frees: ((string * sort) * typ) list * ((string * typ) * term) list ->
+    term -> term
   val instantiateT_same: ((indexname * sort) * typ) list -> typ Same.operation
   val instantiate_same: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
     term Same.operation
@@ -92,6 +98,42 @@
 fun generalize names i tm = Same.commit (generalize_same names i) tm;
 
 
+(* instantiation of free variables (types before terms) *)
+
+fun instantiateT_frees_same [] _ = raise Same.SAME
+  | instantiateT_frees_same instT ty =
+      let
+        fun subst (Type (a, Ts)) = Type (a, Same.map subst Ts)
+          | subst (TFree v) =
+              (case AList.lookup (op =) instT v of
+                SOME T => T
+              | NONE => raise Same.SAME)
+          | subst _ = raise Same.SAME;
+      in subst ty end;
+
+fun instantiate_frees_same ([], []) _ = raise Same.SAME
+  | instantiate_frees_same (instT, inst) tm =
+      let
+        val substT = instantiateT_frees_same instT;
+        fun subst (Const (c, T)) = Const (c, substT T)
+          | subst (Free (x, T)) =
+              let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
+                (case AList.lookup (op =) inst (x, T') of
+                   SOME t => t
+                 | NONE => if same then raise Same.SAME else Free (x, T'))
+              end
+          | subst (Var (xi, T)) = Var (xi, substT T)
+          | subst (Bound _) = raise Same.SAME
+          | subst (Abs (x, T, t)) =
+              (Abs (x, substT T, Same.commit subst t)
+                handle Same.SAME => Abs (x, T, subst t))
+          | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
+      in subst tm end;
+
+fun instantiateT_frees instT ty = Same.commit (instantiateT_frees_same instT) ty;
+fun instantiate_frees inst tm = Same.commit (instantiate_frees_same inst) tm;
+
+
 (* instantiation of schematic variables (types before terms) -- recomputes maxidx *)
 
 local
diff -r 4fa9d5ef95bc -r f7e37a94caee src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Feb 23 10:52:31 2018 +0000
+++ b/src/Pure/thm.ML	Fri Feb 23 15:17:51 2018 +0100
@@ -75,6 +75,7 @@
   exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option
   val theory_of_cterm: cterm -> theory
   val theory_of_thm: thm -> theory
+  val trim_context_ctyp: ctyp -> ctyp
   val trim_context_cterm: cterm -> cterm
   val trim_context: thm -> thm
   val transfer_cterm: theory -> cterm -> cterm
@@ -118,6 +119,8 @@
   val equal_elim: thm -> thm -> thm
   val flexflex_rule: Proof.context option -> thm -> thm Seq.seq
   val generalize: string list * string list -> int -> thm -> thm
+  val generalize_cterm: string list * string list -> int -> cterm -> cterm
+  val generalize_ctyp: string list -> int -> ctyp -> ctyp
   val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
     thm -> thm
   val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
@@ -410,6 +413,13 @@
   Context.certificate_theory (cert_of th)
     handle ERROR msg => raise CONTEXT (msg, [], [], [th], NONE);
 
+fun trim_context_ctyp cT =
+  (case cT of
+    Ctyp {cert = Context.Certificate_Id _, ...} => cT
+  | Ctyp {cert = Context.Certificate thy, T, maxidx, sorts} =>
+      Ctyp {cert = Context.Certificate_Id (Context.theory_id thy),
+        T = T, maxidx = maxidx, sorts = sorts});
+
 fun trim_context_cterm ct =
   (case ct of
     Cterm {cert = Context.Certificate_Id _, ...} => ct
@@ -1152,6 +1162,23 @@
           prop = prop'})
       end;
 
+fun generalize_cterm ([], []) _ ct = ct
+  | generalize_cterm (tfrees, frees) idx (ct as Cterm {cert, t, T, maxidx, sorts}) =
+      if idx <= maxidx then raise CTERM ("generalize_cterm: bad index", [ct])
+      else
+        Cterm {cert = cert, sorts = sorts,
+          T = Term_Subst.generalizeT tfrees idx T,
+          t = Term_Subst.generalize (tfrees, frees) idx t,
+          maxidx = Int.max (maxidx, idx)};
+
+fun generalize_ctyp [] _ cT = cT
+  | generalize_ctyp tfrees idx (Ctyp {cert, T, maxidx, sorts}) =
+      if idx <= maxidx then raise CTERM ("generalize_ctyp: bad index", [])
+      else
+        Ctyp {cert = cert, sorts = sorts,
+          T = Term_Subst.generalizeT tfrees idx T,
+          maxidx = Int.max (maxidx, idx)};
+
 
 (*Instantiation of schematic variables
            A