--- 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