src/Pure/theory.ML

   let
     val pp = Sign.pp thy;
     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 =>
       if member (op =) lhs_vars v then I else insert (op =) v | _ => I)) rhs [];
     val _ =

   let
     val declT =
       (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 ",
         Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Sign.pretty_typ thy T)],
         Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;