# HG changeset patch
# User wenzelm
# Date 771152534 -7200
# Node ID ab09293bccc7052e99460541dd444e819a83014b
# Parent  6bb9eb9cb02f8527f1ea6f4f9cd1edabfec27eca
workaround bug in Type.expand_typ;

diff -r 6bb9eb9cb02f -r ab09293bccc7 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Jun 09 11:00:37 1994 +0200
+++ b/src/Pure/sign.ML	Thu Jun 09 11:02:14 1994 +0200
@@ -362,9 +362,15 @@
   (c, read_raw_typ syn tsig (K None) ty_src, mx)
     handle ERROR => err_in_const (const_name c mx);
 
+(* FIXME move *)
+fun no_tvars ty =
+  if null (typ_tvars ty) then ty
+  else raise_type "Illegal schematic type variable(s)" [ty] [];
+
 fun ext_cnsts rd_const syn_only (syn, tsig, ctab) raw_consts =
   let
-    fun prep_const (c, ty, mx) = (c, cert_typ tsig (varify_typ ty), mx)
+    (* FIXME clean *)
+    fun prep_const (c, ty, mx) = (c, varify_typ (cert_typ tsig (no_tvars ty)), mx)
       handle TYPE (msg, _, _) => (writeln msg; err_in_const (const_name c mx));
 
     val consts = map (prep_const o rd_const syn tsig) raw_consts;