--- a/src/HOL/Tools/Function/function_common.ML Mon May 17 15:11:25 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Mon May 17 23:54:15 2010 +0200
@@ -341,21 +341,19 @@
local
- structure P = OuterParse and K = OuterKeyword
-
- val option_parser = P.group "option"
- ((P.reserved "sequential" >> K Sequential)
- || ((P.reserved "default" |-- P.term) >> Default)
- || (P.reserved "domintros" >> K DomIntros)
- || (P.reserved "no_partials" >> K No_Partials)
- || (P.reserved "tailrec" >> K Tailrec))
+ val option_parser = Parse.group "option"
+ ((Parse.reserved "sequential" >> K Sequential)
+ || ((Parse.reserved "default" |-- Parse.term) >> Default)
+ || (Parse.reserved "domintros" >> K DomIntros)
+ || (Parse.reserved "no_partials" >> K No_Partials)
+ || (Parse.reserved "tailrec" >> K Tailrec))
fun config_parser default =
- (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 option_parser) --| P.$$$ ")") [])
+ (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") [])
>> (fn opts => fold apply_opt opts default)
in
fun function_parser default_cfg =
- config_parser default_cfg -- P.fixes -- Parse_Spec.where_alt_specs
+ config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs
end