src/Pure/sign.ML

 
 (* add constants *)
 
 fun gen_add_consts prep_typ raw_args thy =
   let
-    val prepT = compress_type o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
+    val prepT = Compress.typ thy o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
     fun prep (c, T, mx) = ((c, prepT T, mx) handle TYPE (msg, _, _) => error msg)
       handle ERROR => error ("in declaration of constant " ^ quote (Syntax.const_name c mx));
     val args = map prep raw_args;
     val decls = args |> map (fn (c, T, mx) => (Syntax.const_name c mx, (T, stamp ())));