src/Pure/Isar/element.ML

 
 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
+      in if T = T' then I else insert (eq_fst (op =)) (a, T') end
     | _ => I) th [];
 
 fun instT_thm thy env th =
   if Symtab.is_empty env then th
   else

     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 =
-        (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 = 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 #>