src/Pure/more_thm.ML

--- a/src/Pure/more_thm.ML	Thu Jul 09 22:36:11 2009 +0200
+++ b/src/Pure/more_thm.ML	Thu Jul 09 22:48:12 2009 +0200
@@ -274,7 +274,7 @@
     val instT0 = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
     val instT = map (fn (v, T) => (certT (TVar v), certT T)) instT0;
     val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
-      let val T' = TermSubst.instantiateT instT0 T
+      let val T' = Term_Subst.instantiateT instT0 T
       in (cert (Var ((a, i), T')), cert (Free ((a, T')))) end);
   in Thm.instantiate (instT, inst) th end;