# HG changeset patch
# User wenzelm
# Date 1147481503 -7200
# Node ID 4445b353f78b32ebd9883549d9518fd1228a022d
# Parent  d370c3f5d3b22954ad3e2d19b6dd245f7e57bd44
'defs': unchecked flag;

diff -r d370c3f5d3b2 -r 4445b353f78b src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat May 13 02:51:42 2006 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat May 13 02:51:43 2006 +0200
@@ -181,9 +181,15 @@
   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
     (Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_axioms));
 
+val opt_unchecked_overloaded =
+  Scan.optional (P.$$$ "(" |-- P.!!!
+    (((P.$$$ "unchecked" >> K true) -- Scan.optional (P.$$$ "overloaded" >> K true) false ||
+      P.$$$ "overloaded" >> K (false, true)) --| P.$$$ ")")) (false, false);
+
 val defsP =
   OuterSyntax.command "defs" "define constants" K.thy_decl
-    (opt_overloaded -- Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_defs));
+    (opt_unchecked_overloaded -- Scan.repeat1 P.spec_name
+      >> (Toplevel.theory o IsarThy.add_defs));
 
 
 (* constant definitions and abbreviations *)
@@ -870,7 +876,7 @@
   "begin", "binder", "concl", "constrains", "defines", "fixes",
   "imports", "in", "includes", "infix", "infixl", "infixr", "is",
   "notes", "obtains", "open", "output", "overloaded", "shows",
-  "structure", "uses", "where", "|", "\\<equiv>",
+  "structure", "unchecked", "uses", "where", "|", "\\<equiv>",
   "\\<leftharpoondown>", "\\<rightharpoonup>",
   "\\<rightleftharpoons>", "\\<subseteq>"];