diff -r 854404b8f738 -r f860b7a98445 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/Pure/theory.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -240,7 +240,7 @@
     val consts = Sign.consts_of thy;
     fun prep const =
       let val Const (c, T) = Sign.no_vars pp (Const const)
-      in (c, Consts.typargs consts (c, Compress.typ thy (Type.varifyT T))) end;
+      in (c, Consts.typargs consts (c, Compress.typ thy (Logic.varifyT T))) end;
 
     val lhs_vars = Term.add_tfreesT (#2 lhs) [];
     val rhs_extras = fold (#2 #> Term.fold_atyps (fn TFree v =>
@@ -267,7 +267,7 @@
       (case Sign.const_constraint thy c of
         NONE => error ("Undeclared constant " ^ quote c)
       | SOME declT => declT);
-    val T' = Type.varifyT T;
+    val T' = Logic.varifyT T;
 
     fun message txt =
       [Pretty.block [Pretty.str "Specification of constant ",