src/Pure/sign.ML
changeset 16988 02cd0c8b96d9
parent 16941 0bda949449ee
child 17037 bd15f69bd947
     1.1 --- a/src/Pure/sign.ML	Mon Aug 01 19:20:41 2005 +0200
     1.2 +++ b/src/Pure/sign.ML	Mon Aug 01 19:20:42 2005 +0200
     1.3 @@ -672,7 +672,7 @@
     1.4  
     1.5  fun gen_add_consts prep_typ raw_args thy =
     1.6    let
     1.7 -    val prepT = compress_type o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
     1.8 +    val prepT = Compress.typ thy o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
     1.9      fun prep (c, T, mx) = ((c, prepT T, mx) handle TYPE (msg, _, _) => error msg)
    1.10        handle ERROR => error ("in declaration of constant " ^ quote (Syntax.const_name c mx));
    1.11      val args = map prep raw_args;