# HG changeset patch
# User huffman
# Date 1287857066 25200
# Node ID 4d1a8fa8cdfd09eeffdc8ea768ed3986cfd79bba
# Parent  5325a062ff538c3b73cd895ab6c91c6bd5e8b0a8
change fixrec parser to not accept theorem names with (unchecked) option

diff -r 5325a062ff53 -r 4d1a8fa8cdfd src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Sat Oct 23 11:03:50 2010 -0700
+++ b/src/HOLCF/Tools/fixrec.ML	Sat Oct 23 11:04:26 2010 -0700
@@ -393,10 +393,16 @@
 (******************************** Parsers ********************************)
 (*************************************************************************)
 
+val opt_thm_name' : (bool * Attrib.binding) parser =
+  Parse.$$$ "(" -- Parse.$$$ "unchecked" -- Parse.$$$ ")" >> K (true, Attrib.empty_binding)
+    || Parse_Spec.opt_thm_name ":" >> pair false;
+
+val spec' : (bool * (Attrib.binding * string)) parser =
+  opt_thm_name' -- Parse.prop >> (fn ((a, b), c) => (a, (b, c)));
+
 val alt_specs' : (bool * (Attrib.binding * string)) list parser =
-  Parse.enum1 "|"
-    (Parse.opt_keyword "unchecked" -- Parse_Spec.spec --|
-      Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
+  let val unexpected = Scan.ahead (Parse.name || Parse.$$$ "[" || Parse.$$$ "(");
+  in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (Parse.$$$ "|"))) end;
 
 val _ =
   Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl