some performance tuning via Term_Subst/Same.operation;
tuned;

--- a/src/Pure/Isar/element.ML	Sat Nov 05 18:58:40 2011 +0100
+++ b/src/Pure/Isar/element.ML	Sat Nov 05 19:47:22 2011 +0100
@@ -341,7 +341,7 @@
       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 (Term.fold_atyps (fn TFree v => add_inst v | _ => I))
+      (Term.fold_types o Term.fold_atyps) (fn TFree v => add_inst v | _ => I)
         (Thm.full_prop_of th) [];
   in
     th
@@ -365,19 +365,26 @@
 
 (* instantiate types *)
 
-fun instT_type env =
-  if Symtab.is_empty env then I
-  else Term.map_type_tfree (fn (x, S) => the_default (TFree (x, S)) (Symtab.lookup env x));
+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 env =
-  if Symtab.is_empty env then I
-  else Term.map_types (instT_type env);
+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 (op =) (a, T') end
-  | _ => I) th [];
+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 (op =) (a, T') end
+    | _ => I) th [];
 
 fun instT_thm thy env th =
   if Symtab.is_empty env then th
@@ -400,32 +407,26 @@
 fun inst_term (envT, env) =
   if Symtab.is_empty env then instT_term envT
   else
-    let
-      val instT = instT_type envT;
-      fun inst (Const (x, T)) = Const (x, instT T)
-        | inst (Free (x, T)) =
-            (case Symtab.lookup env x of
-              NONE => Free (x, instT T)
-            | SOME t => t)
-        | inst (Var (xi, T)) = Var (xi, instT T)
-        | inst (b as Bound _) = b
-        | inst (Abs (x, T, t)) = Abs (x, instT T, inst t)
-        | inst (t $ u) = inst t $ inst u;
-    in Envir.beta_norm o inst end;
+    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_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 = (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 [];
+      val subst =
+        (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 [];
     in
       if null substT andalso null subst then th
       else th |> hyps_rule
@@ -434,19 +435,20 @@
         Conv.fconv_rule (Thm.beta_conversion true))
     end;
 
-fun inst_morphism thy envs =
+fun inst_morphism thy (envT, env) =
   let val thy_ref = Theory.check_thy thy in
     Morphism.morphism
      {binding = [],
-      typ = [instT_type (#1 envs)],
-      term = [inst_term envs],
-      fact = [map (fn th => inst_thm (Theory.deref thy_ref) envs th)]}
+      typ = [instT_type envT],
+      term = [inst_term (envT, env)],
+      fact = [map (fn th => inst_thm (Theory.deref thy_ref) (envT, env) th)]}
   end;
 
 
 (* satisfy hypotheses *)
 
-fun satisfy_thm witns thm = thm |> fold (fn hyp =>
+fun satisfy_thm witns thm =
+  thm |> fold (fn hyp =>
     (case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of
       NONE => I
     | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm));