--- a/src/Doc/Isar_Ref/HOL_Specific.thy Mon May 30 14:15:44 2016 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Mon May 30 20:58:16 2016 +0200
@@ -264,12 +264,11 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) primrec} @{syntax "fixes"} @'where' @{syntax multi_specs}
+ @@{command (HOL) primrec} @{syntax specification}
;
- (@@{command (HOL) fun} | @@{command (HOL) function}) function_opts? \<newline>
- @{syntax "fixes"} @'where' @{syntax multi_specs}
+ (@@{command (HOL) fun} | @@{command (HOL) function}) opts? @{syntax specification}
;
- function_opts: '(' (('sequential' | 'domintros') + ',') ')'
+ opts: '(' (('sequential' | 'domintros') + ',') ')'
;
@@{command (HOL) termination} @{syntax term}?
;
@@ -563,8 +562,8 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) partial_function} '(' @{syntax name} ')' \<newline>
- @{syntax "fixes"} @'where' @{syntax multi_specs}
+ @@{command (HOL) partial_function} '(' @{syntax name} ')'
+ @{syntax specification}
\<close>}
\<^descr> @{command (HOL) "partial_function"}~\<open>(mode)\<close> defines
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Mon May 30 14:15:44 2016 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Mon May 30 20:58:16 2016 +0200
@@ -469,6 +469,8 @@
@{syntax thmdecl}? @{syntax prop} @{syntax spec_prems} @{syntax for_fixes}
;
@{syntax_def spec_prems}: (@'if' ((@{syntax prop}+) + @'and'))?
+ ;
+ @{syntax_def specification}: @{syntax "fixes"} @'where' @{syntax multi_specs}
\<close>}
\<close>
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon May 30 14:15:44 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon May 30 20:58:16 2016 +0200
@@ -687,8 +687,7 @@
val _ = Outer_Syntax.local_theory @{command_keyword primrec}
"define primitive recursive functions"
((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser)
- --| @{keyword ")"}) []) --
- (Parse.fixes -- Parse_Spec.where_multi_specs)
+ --| @{keyword ")"}) []) -- Parse_Spec.specification
>> (fn (opts, (fixes, specs)) => snd o primrec_cmd opts fixes specs));
end;
--- a/src/HOL/Tools/Function/fun.ML Mon May 30 14:15:44 2016 +0200
+++ b/src/HOL/Tools/Function/fun.ML Mon May 30 20:58:16 2016 +0200
@@ -174,6 +174,6 @@
Outer_Syntax.local_theory' @{command_keyword fun}
"define general recursive functions (short version)"
(function_parser fun_config
- >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
+ >> (fn (config, (fixes, specs)) => add_fun_cmd fixes specs config))
end
--- a/src/HOL/Tools/Function/function.ML Mon May 30 14:15:44 2016 +0200
+++ b/src/HOL/Tools/Function/function.ML Mon May 30 20:58:16 2016 +0200
@@ -274,7 +274,7 @@
Outer_Syntax.local_theory_to_proof' @{command_keyword function}
"define general recursive functions"
(function_parser default_config
- >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
+ >> (fn (config, (fixes, specs)) => function_cmd fixes specs config))
val _ =
Outer_Syntax.local_theory_to_proof @{command_keyword termination}
--- a/src/HOL/Tools/Function/function_common.ML Mon May 30 14:15:44 2016 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Mon May 30 20:58:16 2016 +0200
@@ -99,8 +99,7 @@
val import_last_function : Proof.context -> info option
val default_config : function_config
val function_parser : function_config ->
- ((function_config * (binding * string option * mixfix) list) *
- Specification.multi_specs_cmd) parser
+ (function_config * ((binding * string option * mixfix) list * Specification.multi_specs_cmd)) parser
end
structure Function_Common : FUNCTION_COMMON =
@@ -374,7 +373,7 @@
>> (fn opts => fold apply_opt opts default)
in
fun function_parser default_cfg =
- config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_multi_specs
+ config_parser default_cfg -- Parse_Spec.specification
end
--- a/src/Pure/Isar/parse_spec.ML Mon May 30 14:15:44 2016 +0200
+++ b/src/Pure/Isar/parse_spec.ML Mon May 30 20:58:16 2016 +0200
@@ -14,6 +14,8 @@
val if_assumes: string list parser
val multi_specs: Specification.multi_specs_cmd parser
val where_multi_specs: Specification.multi_specs_cmd parser
+ val specification:
+ ((binding * string option * mixfix) list * Specification.multi_specs_cmd) parser
val constdecl: (binding * string option * mixfix) parser
val includes: (xstring * Position.T) list parser
val locale_fixes: (binding * string option * mixfix) list parser
@@ -65,6 +67,8 @@
val where_multi_specs = Parse.where_ |-- Parse.!!! multi_specs;
+val specification = Parse.fixes -- where_multi_specs;
+
(* basic constant specifications *)