src/Pure/Isar/rule_insts.ML

--- a/src/Pure/Isar/rule_insts.ML	Tue Sep 12 12:12:39 2006 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Tue Sep 12 12:12:46 2006 +0200
@@ -40,7 +40,7 @@
   end;
 
 fun instantiate inst =
-  Term.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
+  TermSubst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
   Envir.beta_norm;
 
 fun make_instT f v =
@@ -88,7 +88,7 @@
       end;
 
     val type_insts1 = map readT type_insts;
-    val instT1 = Term.instantiateT type_insts1;
+    val instT1 = TermSubst.instantiateT type_insts1;
     val vars1 = map (apsnd instT1) vars;