src/Pure/sign.ML

--- a/src/Pure/sign.ML	Wed Jun 07 02:01:27 2006 +0200
+++ b/src/Pure/sign.ML	Wed Jun 07 02:01:28 2006 +0200
@@ -721,7 +721,7 @@
 
 fun gen_add_consts prep_typ authentic raw_args thy =
   let
-    val prepT = Compress.typ thy o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
+    val prepT = Compress.typ thy o Logic.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
     fun prep (raw_c, raw_T, raw_mx) =
       let
         val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
@@ -755,7 +755,7 @@
 
     val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
     val c' = Syntax.constN ^ full_name thy c;
-    val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg)
+    val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
     val T = Term.fastype_of t;
   in
@@ -772,7 +772,7 @@
   let
     val c = int_const thy raw_c;
     fun prepT raw_T =
-      let val T = Type.varifyT (Type.no_tvars (Term.no_dummyT (prep_typ thy raw_T)))
+      let val T = Logic.varifyT (Type.no_tvars (Term.no_dummyT (prep_typ thy raw_T)))
       in cert_term thy (Const (c, T)); T end
       handle TYPE (msg, _, _) => error msg;
   in thy |> map_consts (Consts.constrain (c, Option.map prepT opt_T)) end;