# HG changeset patch
# User wenzelm
# Date 1464634696 -7200
# Node ID 4d04e14d7ab8a0ccf10081a0177b2c3ed8b7863f
# Parent  b065b4833092fec412841081217e58522f04e837
tuned;

diff -r b065b4833092 -r 4d04e14d7ab8 src/Doc/Isar_Ref/HOL_Specific.thy
--- 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
diff -r b065b4833092 -r 4d04e14d7ab8 src/Doc/Isar_Ref/Outer_Syntax.thy
--- 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>
 
diff -r b065b4833092 -r 4d04e14d7ab8 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- 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;
diff -r b065b4833092 -r 4d04e14d7ab8 src/HOL/Tools/Function/fun.ML
--- 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
diff -r b065b4833092 -r 4d04e14d7ab8 src/HOL/Tools/Function/function.ML
--- 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}
diff -r b065b4833092 -r 4d04e14d7ab8 src/HOL/Tools/Function/function_common.ML
--- 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
 
 
diff -r b065b4833092 -r 4d04e14d7ab8 src/Pure/Isar/parse_spec.ML
--- 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 *)