Temporarily avoid type errors in parse phase.

--- a/src/FOL/ex/NewLocaleTest.thy	Tue Dec 23 14:29:27 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Tue Dec 30 08:18:54 2008 +0100
@@ -110,6 +110,22 @@
 locale use_decl = logic + semi "op ||"
 print_locale! use_decl thm use_decl_def
 
+locale extra_type =
+  fixes a :: 'a
+    and P :: "'a => 'b => o"
+begin
+
+definition test :: "'a => o" where
+  "test(x) <-> (ALL b. P(x, b))"
+
+end
+
+term extra_type.test thm extra_type.test_def
+
+interpretation var: extra_type "0" "%x y. x = 0" .
+
+thm var.test_def
+
 
 section {* Foundational versions of theorems *}
 

--- a/src/Pure/consts.ML	Tue Dec 23 14:29:27 2008 +0100
+++ b/src/Pure/consts.ML	Tue Dec 30 08:18:54 2008 +0100
@@ -275,8 +275,8 @@
     val T = Term.fastype_of rhs;
     val lhs = Const (NameSpace.full_name naming b, T);
 
-    fun err msg = error (msg ^ " on rhs of abbreviation:\n" ^
-      Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs)));
+    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