more standard instantiate operations, where substitutions are already certified and stored with trimmed theory certificate;

--- a/src/Pure/Isar/class_declaration.ML	Wed Feb 21 18:41:41 2018 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Wed Feb 21 20:13:42 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)

--- a/src/Pure/Isar/element.ML	Wed Feb 21 18:41:41 2018 +0100
+++ b/src/Pure/Isar/element.ML	Wed Feb 21 20:13:42 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
@@ -344,115 +344,12 @@
   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 *)

--- a/src/Pure/Isar/expression.ML	Wed Feb 21 18:41:41 2018 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Feb 21 20:13:42 2018 +0100
@@ -171,7 +171,7 @@
     (* parameters *)
     val type_parms = fold Term.add_tfreesT parm_types [];
 
-    (* type inference and context *)
+    (* 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' [];
     val checked =
@@ -179,19 +179,20 @@
       |> Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt)
     val (type_parms'', insts'') = chop (length type_parms') checked;
 
-    val ctxt' = ctxt |> fold Variable.auto_fixes 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 instT =
       (type_parms ~~ map Logic.dest_type type_parms'')
-      |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (#1 v, T))
-      |> Symtab.make;
-    val inst =
-      (parm_names ~~ insts'')
-      |> filter (fn (a, Free (b, _)) => a <> b | _ => true)
-      |> Symtab.make;
+      |> 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;