# HG changeset patch
# User ballarin
# Date 1230621534 -3600
# Node ID 8f84a608883d24a8ede1a0052e696c40cedd2a81
# Parent  96b1b4d5157d1d5d88f17c0246e1abb1ea523dd5
Temporarily avoid type errors in parse phase.

diff -r 96b1b4d5157d -r 8f84a608883d src/FOL/ex/NewLocaleTest.thy
--- 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 *}
 
diff -r 96b1b4d5157d -r 8f84a608883d src/Pure/consts.ML
--- 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