src/HOLCF/Tools/fixrec.ML

 
 (*************************************************************************)
 (******************************** 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
     (Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs')
       >> (fn (fixes, specs) => add_fixrec_cmd fixes specs));