# HG changeset patch
# User wenzelm
# Date 1236270937 -3600
# Node ID cf89a03ee30870eead153f9ec15a2c31249faf60
# Parent  a135bfab6e834813668a496871d76fed92c92f65
Consts.abbreviate: reject schematic term variables, prevent schematic type variables (hidden polymorphism) via Term.close_schematic_term -- see also 8f84a608883d;

diff -r a135bfab6e83 -r cf89a03ee308 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Thu Mar 05 17:09:07 2009 +0100
+++ b/src/Pure/consts.ML	Thu Mar 05 17:35:37 2009 +0100
@@ -264,17 +264,16 @@
     val expand_term = certify pp tsig true consts;
     val force_expand = mode = PrintMode.internal;
 
+    val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
+      error ("Illegal schematic variables on rhs of abbreviation: " ^ Binding.str_of b);
+
     val rhs = raw_rhs
       |> Term.map_types (Type.cert_typ tsig)
-      |> cert_term;
+      |> cert_term
+      |> Term.close_schematic_term;
     val normal_rhs = expand_term rhs;
     val T = Term.fastype_of rhs;
     val lhs = Const (NameSpace.full_name naming b, T);
-
-    fun err msg = (warning (* FIXME should be error *) (msg ^ " on rhs of abbreviation:\n" ^
-      Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs))); true);
-    val _ = Term.exists_subterm Term.is_Var rhs andalso err "Illegal schematic variables";
-    val _ = null (Term.hidden_polymorphism rhs) orelse err "Extra type variables";
   in
     consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
       let