# HG changeset patch
# User wenzelm
# Date 1464634734 -7200
# Node ID dd6cd88cebd97776a17f237b9446e215340be324
# Parent  d191892b1c23dffd7eb70376dcc873a42c96c7cc# Parent  4d04e14d7ab8a0ccf10081a0177b2c3ed8b7863f
merged

diff -r d191892b1c23 -r dd6cd88cebd9 NEWS
--- a/NEWS	Sun May 29 14:43:18 2016 +0200
+++ b/NEWS	Mon May 30 20:58:54 2016 +0200
@@ -66,9 +66,13 @@
 
 *** Isar ***
 
-* Many specification elements support structured statements with 'if'
-eigen-context, e.g. 'axiomatization', 'definition', 'inductive',
-'function'.
+* Command 'axiomatization' has become more restrictive to correspond
+better to internal axioms as singleton facts with mandatory name. Minor
+INCOMPATIBILITY.
+
+* Many specification elements support structured statements with 'if' /
+'for' eigen-context, e.g. 'axiomatization', 'abbreviation',
+'definition', 'inductive', 'function'.
 
 * Toplevel theorem statements support eigen-context notation with 'if' /
 'for' (in postix), which corresponds to 'assumes' / 'fixes' in the
diff -r d191892b1c23 -r dd6cd88cebd9 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sun May 29 14:43:18 2016 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon May 30 20:58:54 2016 +0200
@@ -109,9 +109,7 @@
     (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
       @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
       @{syntax "fixes"} @{syntax "for_fixes"} \<newline>
-      (@'where' clauses)? (@'monos' @{syntax thms})?
-    ;
-    clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
+      (@'where' @{syntax multi_specs})? (@'monos' @{syntax thms})?
     ;
     @@{command print_inductives} ('!'?)
     ;
@@ -266,15 +264,11 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) primrec} @{syntax "fixes"} @'where' equations
-    ;
-    (@@{command (HOL) fun} | @@{command (HOL) function}) functionopts?
-      @{syntax "fixes"} \<newline> @'where' equations
+    @@{command (HOL) primrec} @{syntax specification}
     ;
-
-    equations: (@{syntax thmdecl}? @{syntax prop} + '|')
+    (@@{command (HOL) fun} | @@{command (HOL) function}) opts? @{syntax specification}
     ;
-    functionopts: '(' (('sequential' | 'domintros') + ',') ')'
+    opts: '(' (('sequential' | 'domintros') + ',') ')'
     ;
     @@{command (HOL) termination} @{syntax term}?
     ;
@@ -568,8 +562,8 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) partial_function} '(' @{syntax name} ')' @{syntax "fixes"} \<newline>
-      @'where' @{syntax thmdecl}? @{syntax prop}
+    @@{command (HOL) partial_function} '(' @{syntax name} ')'
+      @{syntax specification}
   \<close>}
 
   \<^descr> @{command (HOL) "partial_function"}~\<open>(mode)\<close> defines
diff -r d191892b1c23 -r dd6cd88cebd9 src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Sun May 29 14:43:18 2016 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Mon May 30 20:58:54 2016 +0200
@@ -450,6 +450,31 @@
 \<close>
 
 
+subsection \<open>Structured specifications\<close>
+
+text \<open>
+  Structured specifications use propositions with explicit notation for the
+  ``eigen-context'' to describe rule structure: \<open>\<And>x. A x \<Longrightarrow> \<dots> \<Longrightarrow> B x\<close> is
+  expressed as \<^theory_text>\<open>B x if A x and \<dots> for x\<close>. It is also possible to use dummy
+  terms ``\<open>_\<close>'' (underscore) to refer to locally fixed variables anonymously.
+
+  Multiple specifications are delimited by ``\<open>|\<close>'' to emphasize separate
+  cases: each with its own scope of inferred types for free variables.
+
+
+  @{rail \<open>
+    @{syntax_def multi_specs}: (@{syntax structured_spec} + '|')
+    ;
+    @{syntax_def structured_spec}:
+      @{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>
+
+
 section \<open>Diagnostic commands\<close>
 
 text \<open>
diff -r d191892b1c23 -r dd6cd88cebd9 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Sun May 29 14:43:18 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon May 30 20:58:54 2016 +0200
@@ -285,14 +285,18 @@
   ``abbreviation''.
 
   @{rail \<open>
-    @@{command definition} (decl @'where')? @{syntax thmdecl}? @{syntax prop}
+    @@{command definition} decl? definition
     ;
-    @@{command abbreviation} @{syntax mode}? \<newline>
-      (decl @'where')? @{syntax prop}
-    ;
-    decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
+    @@{command abbreviation} @{syntax mode}? decl? abbreviation
     ;
     @@{command print_abbrevs} ('!'?)
+    ;
+    decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? @'where'
+    ;
+    definition: @{syntax thmdecl}? @{syntax prop}
+      @{syntax spec_prems} @{syntax for_fixes}
+    ;
+    abbreviation: @{syntax prop} @{syntax for_fixes}
   \<close>}
 
   \<^descr> \<^theory_text>\<open>definition c where eq\<close> produces an internal definition \<open>c \<equiv> t\<close> according
@@ -337,9 +341,10 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command axiomatization} @{syntax "fixes"}? (@'where' specs)?
+    @@{command axiomatization} @{syntax "fixes"}? (@'where' axiomatization)?
     ;
-    specs: (@{syntax thmdecl}? @{syntax props} + @'and')
+    axiomatization: (@{syntax thmdecl} @{syntax prop} + @'and')
+      @{syntax spec_prems} @{syntax for_fixes}
   \<close>}
 
   \<^descr> \<^theory_text>\<open>axiomatization c\<^sub>1 \<dots> c\<^sub>m where \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces several constants
diff -r d191892b1c23 -r dd6cd88cebd9 src/Doc/Tutorial/Misc/AdvancedInd.thy
--- a/src/Doc/Tutorial/Misc/AdvancedInd.thy	Sun May 29 14:43:18 2016 +0200
+++ b/src/Doc/Tutorial/Misc/AdvancedInd.thy	Mon May 30 20:58:54 2016 +0200
@@ -133,7 +133,7 @@
 *}
 
 axiomatization f :: "nat \<Rightarrow> nat"
-  where f_ax: "f(f(n)) < f(Suc(n))"
+  where f_ax: "f(f(n)) < f(Suc(n))" for n :: nat
 
 text{*
 \begin{warn}
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Mon May 30 20:58:54 2016 +0200
@@ -175,7 +175,7 @@
       Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))))
     val ((_, (_, below_ldef)), lthy) = thy
       |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po})
-      |> Specification.definition NONE []
+      |> Specification.definition NONE [] []
           ((Binding.prefix_name "below_" (Thm.def_binding name), []), below_eqn)
     val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy)
     val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/HOLCF/Tools/domaindef.ML
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Mon May 30 20:58:54 2016 +0200
@@ -138,17 +138,17 @@
     val lthy = thy
       |> Class.instantiation ([full_tname], lhs_tfrees, @{sort domain})
     val ((_, (_, emb_ldef)), lthy) =
-        Specification.definition NONE [] (emb_bind, emb_eqn) lthy
+        Specification.definition NONE [] [] (emb_bind, emb_eqn) lthy
     val ((_, (_, prj_ldef)), lthy) =
-        Specification.definition NONE [] (prj_bind, prj_eqn) lthy
+        Specification.definition NONE [] [] (prj_bind, prj_eqn) lthy
     val ((_, (_, defl_ldef)), lthy) =
-        Specification.definition NONE [] (defl_bind, defl_eqn) lthy
+        Specification.definition NONE [] [] (defl_bind, defl_eqn) lthy
     val ((_, (_, liftemb_ldef)), lthy) =
-        Specification.definition NONE [] (liftemb_bind, liftemb_eqn) lthy
+        Specification.definition NONE [] [] (liftemb_bind, liftemb_eqn) lthy
     val ((_, (_, liftprj_ldef)), lthy) =
-        Specification.definition NONE [] (liftprj_bind, liftprj_eqn) lthy
+        Specification.definition NONE [] [] (liftprj_bind, liftprj_eqn) lthy
     val ((_, (_, liftdefl_ldef)), lthy) =
-        Specification.definition NONE [] (liftdefl_bind, liftdefl_eqn) lthy
+        Specification.definition NONE [] [] (liftdefl_bind, liftdefl_eqn) lthy
     val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy)
     val emb_def = singleton (Proof_Context.export lthy ctxt_thy) emb_ldef
     val prj_def = singleton (Proof_Context.export lthy ctxt_thy) prj_ldef
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/HOLCF/Tools/fixrec.ML
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Mon May 30 20:58:54 2016 +0200
@@ -334,7 +334,7 @@
     val (skips, raw_spec) = ListPair.unzip raw_spec'
     val (fixes : ((binding * typ) * mixfix) list,
          spec : (Attrib.binding * term) list) =
-          fst (prep_spec raw_fixes (map (rpair []) raw_spec) lthy)
+          fst (prep_spec raw_fixes (map (fn s => (s, [], [])) raw_spec) lthy)
     val names = map (Binding.name_of o fst o fst) fixes
     fun check_head name =
         member (op =) names name orelse
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy	Mon May 30 20:58:54 2016 +0200
@@ -15,12 +15,29 @@
   append_name :: mname
 
 axiomatization val_nam next_nam l_nam l1_nam l2_nam l3_nam l4_nam :: vnam
-where distinct_fields: "val_name \<noteq> next_name"
-  and distinct_vars:
-  "l_nam \<noteq> l1_nam" "l_nam \<noteq> l2_nam" "l_nam \<noteq> l3_nam" "l_nam \<noteq> l4_nam"
-  "l1_nam \<noteq> l2_nam" "l1_nam \<noteq> l3_nam" "l1_nam \<noteq> l4_nam"
-  "l2_nam \<noteq> l3_nam" "l2_nam \<noteq> l4_nam"
-  "l3_nam \<noteq> l4_nam"
+where distinct_fields: "val_nam \<noteq> next_nam"
+  and distinct_vars1: "l_nam \<noteq> l1_nam"
+  and distinct_vars2: "l_nam \<noteq> l2_nam"
+  and distinct_vars3: "l_nam \<noteq> l3_nam"
+  and distinct_vars4: "l_nam \<noteq> l4_nam"
+  and distinct_vars5: "l1_nam \<noteq> l2_nam"
+  and distinct_vars6: "l1_nam \<noteq> l3_nam"
+  and distinct_vars7: "l1_nam \<noteq> l4_nam"
+  and distinct_vars8: "l2_nam \<noteq> l3_nam"
+  and distinct_vars9: "l2_nam \<noteq> l4_nam"
+  and distinct_vars10: "l3_nam \<noteq> l4_nam"
+
+lemmas distinct_vars =
+  distinct_vars1
+  distinct_vars2
+  distinct_vars3
+  distinct_vars4
+  distinct_vars5
+  distinct_vars6
+  distinct_vars7
+  distinct_vars8
+  distinct_vars9
+  distinct_vars10
 
 definition list_name :: cname where
   "list_name = Cname list_nam"
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon May 30 20:58:54 2016 +0200
@@ -192,7 +192,7 @@
         thy' |>
         BNF_LFP_Compat.primrec_global
           [(Binding.name swap_name, SOME swapT, NoSyn)]
-          [((Attrib.empty_binding, def1), [])] ||>
+          [((Attrib.empty_binding, def1), [], [])] ||>
         Sign.parent_path ||>>
         Global_Theory.add_defs_unchecked true
           [((Binding.name name, def2), [])] |>> (snd o fst)
@@ -226,7 +226,7 @@
         thy' |>
         BNF_LFP_Compat.primrec_global
           [(Binding.name prm_name, SOME prmT, NoSyn)]
-          (map (fn def => ((Attrib.empty_binding, def), [])) [def1, def2]) ||>
+          (map (fn def => ((Attrib.empty_binding, def), [], [])) [def1, def2]) ||>
         Sign.parent_path
       end) ak_names_types thy3;
     
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Mon May 30 20:58:54 2016 +0200
@@ -255,7 +255,7 @@
             (Free (nth perm_names_types' i) $
                Free ("pi", mk_permT (TFree ("'x", @{sort type}))) $
                list_comb (c, args),
-             list_comb (c, map perm_arg (dts ~~ args))))), [])
+             list_comb (c, map perm_arg (dts ~~ args))))), [], [])
         end) constrs
       end) descr;
 
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Quickcheck_Examples/Hotel_Example.thy
--- a/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Quickcheck_Examples/Hotel_Example.thy	Mon May 30 20:58:54 2016 +0200
@@ -109,9 +109,17 @@
 
 axiomatization find_first' :: "('b Quickcheck_Exhaustive.unknown => 'a Quickcheck_Exhaustive.three_valued)
     => 'b list => 'a Quickcheck_Exhaustive.three_valued"
-where find_first'_code [code]:
-  "find_first' f [] = Quickcheck_Exhaustive.No_value"
-  "find_first' f (x # xs) = (case f (Quickcheck_Exhaustive.Known x) of Quickcheck_Exhaustive.No_value => find_first' f xs | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | Quickcheck_Exhaustive.Unknown_value => (case find_first' f xs of Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x | _ => Quickcheck_Exhaustive.Unknown_value))"
+where find_first'_Nil: "find_first' f [] = Quickcheck_Exhaustive.No_value"
+  and find_first'_Cons: "find_first' f (x # xs) =
+    (case f (Quickcheck_Exhaustive.Known x) of
+      Quickcheck_Exhaustive.No_value => find_first' f xs
+    | Quickcheck_Exhaustive.Value x => Quickcheck_Exhaustive.Value x
+    | Quickcheck_Exhaustive.Unknown_value =>
+        (case find_first' f xs of Quickcheck_Exhaustive.Value x =>
+          Quickcheck_Exhaustive.Value x
+        | _ => Quickcheck_Exhaustive.Unknown_value))"
+
+lemmas find_first'_code [code] = find_first'_Nil find_first'_Cons
 
 axiomatization neg_cps_of_set :: "'a set => ('a Quickcheck_Exhaustive.unknown => term list Quickcheck_Exhaustive.three_valued) => natural => term list Quickcheck_Exhaustive.three_valued"
 where neg_cps_of_set_code [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Mon May 30 20:58:54 2016 +0200
@@ -1020,7 +1020,7 @@
             "\ndoes not match type " ^ ty' ^ " in definition");
         val id' = mk_rulename id;
         val ((t', (_, th)), lthy') = Named_Target.theory_init thy
-          |> Specification.definition NONE []
+          |> Specification.definition NONE [] []
             ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t)));
         val phi =
           Proof_Context.export_morphism lthy'
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/BNF/bnf_axiomatization.ML
--- a/src/HOL/Tools/BNF/bnf_axiomatization.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_axiomatization.ML	Mon May 30 20:58:54 2016 +0200
@@ -81,8 +81,10 @@
     val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
     val all_goalss = map single goals @ (if nwits > 0 then wit_goalss else []);
 
-    val (((_, [raw_thms])), lthy) = Local_Theory.background_theory_result
-      (Specification.axiomatization [] [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy;
+    val (((_, raw_thms)), lthy) = Local_Theory.background_theory_result
+      (Specification.axiomatization [] [] []
+        (map_index (fn (i, ax) =>
+          ((mk_b ("axiom" ^ string_of_int (i + 1)) Binding.empty, []), ax)) (flat all_goalss))) lthy;
 
     fun mk_wit_thms set_maps =
       Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/BNF/bnf_gfp_grec.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Mon May 30 20:58:54 2016 +0200
@@ -265,7 +265,7 @@
     val (([free], [def_free], [simps_free]), (lthy, lthy_old)) = lthy
       |> Local_Theory.open_target |> snd
       |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
-      |> primrec [(b, NONE, NoSyn)] (map (fn eq => ((Attrib.empty_binding, eq), [])) eqs)
+      |> primrec [(b, NONE, NoSyn)] (map (fn eq => ((Attrib.empty_binding, eq), [], [])) eqs)
       ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon May 30 20:58:54 2016 +0200
@@ -1829,7 +1829,7 @@
 
     val ({defname, pelims = [[pelim]], pinducts = [pinduct], psimps = [psimp], ...}, lthy) =
       Function.add_function [(Binding.concealed binding, NONE, NoSyn)]
-        [(((Binding.concealed Binding.empty, []), parsed_eq), [])]
+        [(((Binding.concealed Binding.empty, []), parsed_eq), [], [])]
         Function_Common.default_config pat_completeness_auto lthy;
   in
     ((defname, (pelim, pinduct, psimp)), lthy)
@@ -1982,7 +1982,7 @@
 
     val (plugins, friend, transfer) = get_options lthy opts;
     val ([((b, fun_T), mx)], [(_, eq)]) =
-      fst (Specification.read_multi_specs raw_fixes [((Attrib.empty_binding, raw_eq), [])] lthy);
+      fst (Specification.read_multi_specs raw_fixes [((Attrib.empty_binding, raw_eq), [], [])] lthy);
 
     val _ = Sign.of_sort (Proof_Context.theory_of lthy) (fun_T, @{sort type}) orelse
       error ("Type of " ^ Binding.print b ^ " contains top sort");
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon May 30 20:58:54 2016 +0200
@@ -1588,7 +1588,7 @@
     val (raw_specs, of_specs_opt) =
       split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy));
     val (fixes, specs) =
-      fst (Specification.read_multi_specs raw_fixes (map (rpair []) raw_specs) lthy);
+      fst (Specification.read_multi_specs raw_fixes (map (fn spec => (spec, [], [])) raw_specs) lthy);
   in
     primcorec_ursive auto opts fixes specs of_specs_opt lthy
   end;
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon May 30 20:58:54 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 d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon May 30 20:58:54 2016 +0200
@@ -623,11 +623,11 @@
                 else if Binding.eq_name (b, equal_binding) then
                   pair (Term.lambda u exist_xs_u_eq_ctr, refl)
                 else
-                  Specification.definition (SOME (b, NONE, NoSyn)) []
+                  Specification.definition (SOME (b, NONE, NoSyn)) [] []
                     ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr) #>> apsnd snd)
               ks exist_xs_u_eq_ctrs disc_bindings
             ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
-              Specification.definition (SOME (b, NONE, NoSyn)) []
+              Specification.definition (SOME (b, NONE, NoSyn)) [] []
                 ((Thm.def_binding b, []), sel_spec b proto_sels) #>> apsnd snd) sel_infos
             ||> `Local_Theory.close_target;
 
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Mon May 30 20:58:54 2016 +0200
@@ -93,7 +93,7 @@
           mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})
           |> Syntax.check_term lthy;
         val ((_, (_, raw_def)), lthy') =
-          Specification.definition NONE [] (Attrib.empty_binding, spec) lthy;
+          Specification.definition NONE [] [] (Attrib.empty_binding, spec) lthy;
         val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy');
         val def = singleton (Proof_Context.export lthy' thy_ctxt) raw_def;
       in
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Function/fun.ML	Mon May 30 20:58:54 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 d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Function/function.ML	Mon May 30 20:58:54 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 d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Mon May 30 20:58:54 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 d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Mon May 30 20:58:54 2016 +0200
@@ -226,7 +226,7 @@
         "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
     val Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user} = setup_data;
 
-    val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [(eqn_raw, [])] lthy;
+    val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [(eqn_raw, [], [])] lthy;
     val ((_, plain_eqn), args_ctxt) = Variable.focus NONE eqn lthy;
 
     val ((f_binding, fT), mixfix) = the_single fixes;
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon May 30 20:58:54 2016 +0200
@@ -89,7 +89,7 @@
     val rhs = relcomp_op $ param_rel_fixed $ fixed_crel
     val definition_term = Logic.mk_equals (lhs, rhs)
     fun note_def lthy =
-      Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) []
+      Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) [] []
         ((Binding.empty, []), definition_term) lthy |>> (snd #> snd);
     fun raw_def lthy =
       let
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 30 20:58:54 2016 +0200
@@ -56,7 +56,7 @@
     thy
     |> Class.instantiation ([tyco], vs, @{sort partial_term_of})
     |> `(fn lthy => Syntax.check_term lthy eq)
-    |-> (fn eq => Specification.definition NONE [] ((Binding.name (triv_name_of eq), []), eq))
+    |-> (fn eq => Specification.definition NONE [] [] ((Binding.name (triv_name_of eq), []), eq))
     |> snd
     |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   end
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon May 30 20:58:54 2016 +0200
@@ -365,7 +365,7 @@
       Function.add_function
         (map (fn (name, T) => (Binding.concealed (Binding.name name), SOME T, NoSyn))
           (names ~~ Ts))
-        (map (fn t => (((Binding.concealed Binding.empty, []), t), [])) eqs_t)
+        (map (fn t => (((Binding.concealed Binding.empty, []), t), [], [])) eqs_t)
         Function_Common.default_config pat_completeness_auto
       #> snd
       #> (fn lthy => Function.prove_termination NONE (the termination_tac lthy) lthy)
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon May 30 20:58:54 2016 +0200
@@ -266,7 +266,7 @@
     |> random_aux_specification prfx random_auxN auxs_eqs
     |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
     |-> (fn random_defs' => fold_map (fn random_def =>
-          Specification.definition NONE []
+          Specification.definition NONE [] []
             ((Binding.concealed Binding.empty, []), random_def)) random_defs')
     |> snd
     |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Mon May 30 20:58:54 2016 +0200
@@ -43,7 +43,7 @@
     thy
     |> Class.instantiation ([tyco], vs, @{sort term_of})
     |> `(fn lthy => Syntax.check_term lthy eq)
-    |-> (fn eq => Specification.definition NONE [] ((Binding.name (triv_name_of eq), []), eq))
+    |-> (fn eq => Specification.definition NONE [] [] ((Binding.name (triv_name_of eq), []), eq))
     |> snd
     |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   end;
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/inductive.ML	Mon May 30 20:58:54 2016 +0200
@@ -610,7 +610,7 @@
 
 fun ind_cases_rules ctxt raw_props raw_fixes =
   let
-    val (props, ctxt' ) = Specification.read_props raw_props raw_fixes ctxt;
+    val (props, ctxt') = Specification.read_props raw_props raw_fixes ctxt;
     val rules = Proof_Context.export ctxt' ctxt (map (mk_cases ctxt') props);
   in rules end;
 
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Tools/record.ML	Mon May 30 20:58:54 2016 +0200
@@ -1734,7 +1734,7 @@
     thy
     |> Class.instantiation ([tyco], vs, sort)
     |> `(fn lthy => Syntax.check_term lthy eq)
-    |-> (fn eq => Specification.definition NONE [] ((Binding.concealed Binding.empty, []), eq))
+    |-> (fn eq => Specification.definition NONE [] [] ((Binding.concealed Binding.empty, []), eq))
     |> snd
     |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   end;
@@ -1781,7 +1781,7 @@
       |> fold Code.add_default_eqn simps
       |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
       |> `(fn lthy => Syntax.check_term lthy eq)
-      |-> (fn eq => Specification.definition NONE [] (Attrib.empty_binding, eq))
+      |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
       |-> (fn (_, (_, eq_def)) =>
          Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
       |-> (fn eq_def => fn thy =>
diff -r d191892b1c23 -r dd6cd88cebd9 src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Sun May 29 14:43:18 2016 +0200
+++ b/src/HOL/Typerep.thy	Mon May 30 20:58:54 2016 +0200
@@ -58,7 +58,7 @@
     thy
     |> Class.instantiation ([tyco], vs, @{sort typerep})
     |> `(fn lthy => Syntax.check_term lthy eq)
-    |-> (fn eq => Specification.definition NONE [] (Attrib.empty_binding, eq))
+    |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
     |> snd
     |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   end;
diff -r d191892b1c23 -r dd6cd88cebd9 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Mon May 30 20:58:54 2016 +0200
@@ -12,10 +12,10 @@
   val simple_spec: (Attrib.binding * string) parser
   val simple_specs: (Attrib.binding * string list) parser
   val if_assumes: string list parser
-  val spec: (string list * (Attrib.binding * string)) parser
   val multi_specs: Specification.multi_specs_cmd parser
   val where_multi_specs: Specification.multi_specs_cmd parser
-  val specification: (string list * (Attrib.binding * string list) list) 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
@@ -60,17 +60,14 @@
   Scan.optional (Parse.$$$ "if" |-- Parse.!!! (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat))
     [];
 
-val spec = (opt_thm_name ":" -- Parse.prop) -- if_assumes >> swap;
-
 val multi_specs =
   Parse.enum1 "|"
-    (opt_thm_name ":" -- Parse.prop -- if_assumes --|
+    ((opt_thm_name ":" -- Parse.prop -- if_assumes -- Parse.for_fixes >> Scan.triple1) --|
       Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
 
 val where_multi_specs = Parse.where_ |-- Parse.!!! multi_specs;
 
-val specification =
-  Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.prop) -- if_assumes >> swap;
+val specification = Parse.fixes -- where_multi_specs;
 
 
 (* basic constant specifications *)
diff -r d191892b1c23 -r dd6cd88cebd9 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/Pure/Isar/specification.ML	Mon May 30 20:58:54 2016 +0200
@@ -9,43 +9,42 @@
 sig
   val read_props: string list -> (binding * string option * mixfix) list -> Proof.context ->
     term list * Proof.context
-  val read_prop: string -> (binding * string option * mixfix) list -> Proof.context ->
-    term * Proof.context
-  val check_spec: (binding * typ option * mixfix) list ->
-    term list -> Attrib.binding * term -> Proof.context ->
-    ((((binding * typ) * mixfix) list * (Attrib.binding * term)) * (string -> Position.T))
-      * Proof.context
-  val read_spec: (binding * string option * mixfix) list ->
-    string list -> Attrib.binding * string -> Proof.context ->
-    ((((binding * typ) * mixfix) list * (Attrib.binding * term)) * (string -> Position.T))
-      * Proof.context
-  type multi_specs = ((Attrib.binding * term) * term list) list
-  type multi_specs_cmd = ((Attrib.binding * string) * string list) list
+  val check_spec_open: (binding * typ option * mixfix) list ->
+    (binding * typ option * mixfix) list -> term list -> term -> Proof.context ->
+    ((binding * typ option * mixfix) list * string list * (string -> Position.T) * term) *
+    Proof.context
+  val read_spec_open: (binding * string option * mixfix) list ->
+    (binding * string option * mixfix) list -> string list -> string -> Proof.context ->
+    ((binding * typ option * mixfix) list * string list * (string -> Position.T) * term) *
+    Proof.context
+  type multi_specs =
+    ((Attrib.binding * term) * term list * (binding * typ option * mixfix) list) list
+  type multi_specs_cmd =
+    ((Attrib.binding * string) * string list * (binding * string option * mixfix) list) list
   val check_multi_specs: (binding * typ option * mixfix) list -> multi_specs -> Proof.context ->
     (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
   val read_multi_specs: (binding * string option * mixfix) list -> multi_specs_cmd -> Proof.context ->
     (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
-  val check_specification: (binding * typ option * mixfix) list -> term list ->
-    (Attrib.binding * term list) list -> Proof.context ->
-    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
-  val read_specification: (binding * string option * mixfix) list -> string list ->
-    (Attrib.binding * string list) list -> Proof.context ->
-    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
-  val axiomatization: (binding * typ option * mixfix) list -> term list ->
-    (Attrib.binding * term list) list -> theory -> (term list * thm list list) * theory
-  val axiomatization_cmd: (binding * string option * mixfix) list -> string list ->
-    (Attrib.binding * string list) list -> theory -> (term list * thm list list) * theory
+  val axiomatization: (binding * typ option * mixfix) list ->
+    (binding * typ option * mixfix) list -> term list ->
+    (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
+  val axiomatization_cmd: (binding * string option * mixfix) list ->
+    (binding * string option * mixfix) list -> string list ->
+    (Attrib.binding * string) list -> theory -> (term list * thm list) * theory
   val axiom: Attrib.binding * term -> theory -> thm * theory
-  val definition: (binding * typ option * mixfix) option -> term list ->
-    Attrib.binding * term -> local_theory -> (term * (string * thm)) * local_theory
-  val definition': (binding * typ option * mixfix) option -> term list ->
-    Attrib.binding * term -> bool -> local_theory -> (term * (string * thm)) * local_theory
-  val definition_cmd: (binding * string option * mixfix) option -> string list ->
-    Attrib.binding * string -> bool -> local_theory -> (term * (string * thm)) * local_theory
-  val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option -> term ->
-    bool -> local_theory -> local_theory
-  val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option -> string ->
-    bool -> local_theory -> local_theory
+  val definition: (binding * typ option * mixfix) option ->
+    (binding * typ option * mixfix) list -> term list -> Attrib.binding * term ->
+    local_theory -> (term * (string * thm)) * local_theory
+  val definition': (binding * typ option * mixfix) option ->
+    (binding * typ option * mixfix) list ->  term list -> Attrib.binding * term ->
+    bool -> local_theory -> (term * (string * thm)) * local_theory
+  val definition_cmd: (binding * string option * mixfix) option ->
+    (binding * string option * mixfix) list -> string list -> Attrib.binding * string ->
+    bool -> local_theory -> (term * (string * thm)) * local_theory
+  val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option ->
+    (binding * typ option * mixfix) list -> term -> bool -> local_theory -> local_theory
+  val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option ->
+    (binding * string option * mixfix) list -> string -> bool -> local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list ->
     local_theory -> local_theory
@@ -91,26 +90,35 @@
     val ctxt3 = ctxt2 |> fold Variable.declare_term props3;
   in (props3, ctxt3) end;
 
-fun read_prop raw_prop raw_fixes ctxt =
-  let val ([prop], ctxt') = read_props [raw_prop] raw_fixes ctxt
-  in (prop, ctxt') end;
-
 
 (* prepare specification *)
 
 local
 
-fun close_forms ctxt auto_close i prems concls =
-  if not auto_close andalso null prems then concls
-  else
-    let
-      val xs =
-        if auto_close then rev (fold (Variable.add_free_names ctxt) (prems @ concls) [])
-        else [];
-      val types =
-        map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length xs));
-      val uniform_typing = AList.lookup (op =) (xs ~~ types);
-    in map (Logic.close_prop_constraint uniform_typing (xs ~~ xs) prems) concls end;
+fun prep_decls prep_var raw_vars ctxt =
+  let
+    val (vars, ctxt') = fold_map prep_var raw_vars ctxt;
+    val (xs, ctxt'') = ctxt'
+      |> Context_Position.set_visible false
+      |> Proof_Context.add_fixes vars
+      ||> Context_Position.restore_visible ctxt';
+    val _ =
+      Context_Position.reports ctxt''
+        (map (Binding.pos_of o #1) vars ~~
+          map (Variable.markup_entity_def ctxt'' ##> Properties.remove Markup.kindN) xs);
+  in ((vars, xs), ctxt'') end;
+
+fun close_form ctxt ys prems concl =
+  let val xs = rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) (rev ys));
+  in Logic.close_prop_constraint (Variable.default_type ctxt) (xs ~~ xs) prems concl end;
+
+fun dummy_frees ctxt xs tss =
+  let
+    val names =
+      Variable.names_of ((fold o fold) Variable.declare_term tss ctxt)
+      |> fold Name.declare xs;
+    val (tss', _) = (fold_map o fold_map) Term.free_dummy_patterns tss names;
+  in tss' end;
 
 fun get_positions ctxt x =
   let
@@ -125,99 +133,92 @@
       | get _ _ = [];
   in get [] end;
 
-fun prepare prep_var parse_prop prep_att auto_close raw_vars raw_specss ctxt =
+fun prep_spec_open prep_var parse_prop raw_vars raw_params raw_prems raw_concl ctxt =
   let
-    val (vars, vars_ctxt) = ctxt |> fold_map prep_var raw_vars;
-    val (xs, params_ctxt) = vars_ctxt
-      |> Context_Position.set_visible false
-      |> Proof_Context.add_fixes vars
-      ||> Context_Position.restore_visible vars_ctxt;
-    val _ =
-      Context_Position.reports params_ctxt
-        (map (Binding.pos_of o #1) vars ~~
-          map (Variable.markup_entity_def params_ctxt ##> Properties.remove Markup.kindN) xs);
+    val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt;
+    val (ys, params_ctxt) = vars_ctxt |> fold_map prep_var raw_params |-> Proof_Context.add_fixes;
+
+    val props =
+      map (parse_prop params_ctxt) (raw_concl :: raw_prems)
+      |> singleton (dummy_frees params_ctxt (xs @ ys));
+
+    val concl :: prems = Syntax.check_props params_ctxt props;
+    val spec = Logic.list_implies (prems, concl);
+    val spec_ctxt = Variable.declare_term spec params_ctxt;
 
-    val Asss0 =
-      map (fn (raw_concls, raw_prems) => raw_prems :: map snd raw_concls) raw_specss
-      |> (burrow o burrow) (grouped 10 Par_List.map_independent (parse_prop params_ctxt));
-    val names =
-      Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss0)
-      |> fold Name.declare xs;
+    fun get_pos x =
+      (case maps (get_positions spec_ctxt x) props of
+        [] => Position.none
+      | pos :: _ => pos);
+  in ((vars, xs, get_pos, spec), spec_ctxt) end;
+
+fun prep_specs prep_var parse_prop prep_att raw_vars raw_specss ctxt =
+  let
+    val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt;
 
-    val (Asss1, _) = (fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss0 names;
-    val idx = (fold o fold o fold) Term.maxidx_term Asss1 ~1 + 1;
+    val propss0 =
+      raw_specss |> map (fn ((_, raw_concl), raw_prems, raw_params) =>
+        let val (ys, ctxt') = vars_ctxt |> fold_map prep_var raw_params |-> Proof_Context.add_fixes
+        in (ys, map (pair ctxt') (raw_concl :: raw_prems)) end);
+    val props =
+      burrow (grouped 10 Par_List.map_independent (uncurry parse_prop)) (map #2 propss0)
+      |> dummy_frees vars_ctxt xs
+      |> map2 (fn (ys, _) => fn concl :: prems => close_form vars_ctxt ys prems concl) propss0;
 
-    val (Asss2, _) =
-      fold_map (fn prems :: conclss => fn i =>
-        (burrow (close_forms params_ctxt auto_close i prems) conclss, i + 1)) Asss1 idx;
-
-    val specs = burrow (Syntax.check_props params_ctxt) (flat Asss2);
-    val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
+    val specs = Syntax.check_props vars_ctxt props;
+    val specs_ctxt = vars_ctxt |> fold Variable.declare_term specs;
 
     val ps = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
     val params = map2 (fn (b, _, mx) => fn (_, T) => ((b, T), mx)) vars ps;
     val name_atts: Attrib.binding list =
-      map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (maps #1 raw_specss);
-
-    fun get_pos x =
-      (case (maps o maps o maps) (get_positions specs_ctxt x) Asss2 of
-        [] => Position.none
-      | pos :: _ => pos);
-  in (((params, name_atts ~~ specs), get_pos), specs_ctxt) end;
-
-
-fun single_spec ((a, B), As) = ([(a, [B])], As);
-fun the_spec (a, [prop]) = (a, prop);
-
-fun prep_specs prep_var parse_prop prep_att auto_close vars specs =
-  prepare prep_var parse_prop prep_att auto_close
-    vars (map single_spec specs) #>> (apfst o apsnd) (map the_spec);
+      map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (map #1 raw_specss);
+  in ((params, name_atts ~~ specs), specs_ctxt) end;
 
 in
 
-fun check_spec xs As B =
-  prep_specs Proof_Context.cert_var (K I) (K I) false xs [(B, As)] #>
-  (apfst o apfst o apsnd) the_single;
+val check_spec_open = prep_spec_open Proof_Context.cert_var (K I);
+val read_spec_open = prep_spec_open Proof_Context.read_var Syntax.parse_prop;
 
-fun read_spec xs As B =
-  prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src false xs [(B, As)] #>
-  (apfst o apfst o apsnd) the_single;
-
-type multi_specs = ((Attrib.binding * term) * term list) list;
-type multi_specs_cmd = ((Attrib.binding * string) * string list) list;
+type multi_specs =
+  ((Attrib.binding * term) * term list * (binding * typ option * mixfix) list) list;
+type multi_specs_cmd =
+  ((Attrib.binding * string) * string list * (binding * string option * mixfix) list) list;
 
 fun check_multi_specs xs specs =
-  prep_specs Proof_Context.cert_var (K I) (K I) true xs specs #>> #1;
+  prep_specs Proof_Context.cert_var (K I) (K I) xs specs;
 
 fun read_multi_specs xs specs =
-  prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src true xs specs #>> #1;
-
-fun check_specification xs As Bs =
-  prepare Proof_Context.cert_var (K I) (K I) true xs [(Bs, As)] #>> #1;
-
-fun read_specification xs As Bs =
-  prepare Proof_Context.read_var Syntax.parse_prop Attrib.check_src true xs [(Bs, As)] #>> #1;
+  prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src xs specs;
 
 end;
 
 
 (* axiomatization -- within global theory *)
 
-fun gen_axioms prep raw_decls raw_prems raw_concls thy =
+fun gen_axioms prep_stmt prep_att raw_decls raw_fixes raw_prems raw_concls thy =
   let
-    val ((decls, specs), _) = prep raw_decls raw_prems raw_concls (Proof_Context.init_global thy);
-    val xs = map (fn ((b, T), _) => (Variable.check_name b, T)) decls;
+    (*specification*)
+    val ((vars, [prems, concls], _, _), vars_ctxt) =
+      Proof_Context.init_global thy
+      |> prep_stmt (raw_decls @ raw_fixes) ((map o map) (rpair []) [raw_prems, map snd raw_concls]);
+    val (decls, fixes) = chop (length raw_decls) vars;
+
+    val frees =
+      rev ((fold o fold) (Variable.add_frees vars_ctxt) [prems, concls] [])
+      |> map (fn (x, T) => (x, Free (x, T)));
+    val close = Logic.close_prop (map #2 fixes @ frees) prems;
+    val specs =
+      map ((apsnd o map) (prep_att vars_ctxt) o fst) raw_concls ~~ map close concls;
 
     (*consts*)
-    val (consts, consts_thy) = thy |> fold_map Theory.specify_const decls;
-    val subst = Term.subst_atomic (map Free xs ~~ consts);
+    val (consts, consts_thy) = thy
+      |> fold_map (fn ((b, _, mx), (_, t)) => Theory.specify_const ((b, Term.type_of t), mx)) decls;
+    val subst = Term.subst_atomic (map (#2 o #2) decls ~~ consts);
 
     (*axioms*)
-    val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
-        fold_map Thm.add_axiom_global
-          (map (apfst (fn a => Binding.map_name (K a) b))
-            (Global_Theory.name_multi (Binding.name_of b) (map subst props)))
-        #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
+    val (axioms, axioms_thy) =
+      (specs, consts_thy) |-> fold_map (fn ((b, atts), prop) =>
+        Thm.add_axiom_global (b, subst prop) #>> (fn (_, th) => ((b, atts), [([th], [])])));
 
     (*facts*)
     val (facts, facts_lthy) = axioms_thy
@@ -225,33 +226,33 @@
       |> Spec_Rules.add Spec_Rules.Unknown (consts, maps (maps #1 o #2) axioms)
       |> Local_Theory.notes axioms;
 
-  in ((consts, map #2 facts), Local_Theory.exit_global facts_lthy) end;
+  in ((consts, map (the_single o #2) facts), Local_Theory.exit_global facts_lthy) end;
 
-val axiomatization = gen_axioms check_specification;
-val axiomatization_cmd = gen_axioms read_specification;
+val axiomatization = gen_axioms Proof_Context.cert_stmt (K I);
+val axiomatization_cmd = gen_axioms Proof_Context.read_stmt Attrib.check_src;
 
-fun axiom (b, ax) = axiomatization [] [] [(b, [ax])] #>> (hd o hd o snd);
+fun axiom (b, ax) = axiomatization [] [] [] [(b, ax)] #>> (hd o snd);
 
 
 (* definition *)
 
-fun gen_def prep raw_var raw_prems raw_spec int lthy =
+fun gen_def prep_spec prep_att raw_var raw_params raw_prems ((a, raw_atts), raw_spec) int lthy =
   let
-    val ((vars, ((raw_name, atts), prop)), get_pos) =
-      fst (prep (the_list raw_var) raw_prems raw_spec lthy);
-    val (((x, T), rhs), prove) = Local_Defs.derived_def lthy {conditional = true} prop;
+    val atts = map (prep_att lthy) raw_atts;
+
+    val ((vars, xs, get_pos, spec), spec_ctxt) = lthy
+      |> prep_spec (the_list raw_var) raw_params raw_prems raw_spec;
+    val (((x, T), rhs), prove) = Local_Defs.derived_def lthy {conditional = true} spec;
     val _ = Name.reject_internal (x, []);
     val (b, mx) =
-      (case vars of
-        [] => (Binding.make (x, get_pos x), NoSyn)
-      | [((b, _), mx)] =>
-          let
-            val y = Variable.check_name b;
-            val _ = x = y orelse
-              error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
-                Position.here (Binding.pos_of b));
-          in (b, mx) end);
-    val name = Thm.def_binding_optional b raw_name;
+      (case (vars, xs) of
+        ([], []) => (Binding.make (x, get_pos x), NoSyn)
+      | ([(b, _, mx)], [y]) =>
+          if x = y then (b, mx)
+          else
+            error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
+              Position.here (Binding.pos_of b)));
+    val name = Thm.def_binding_optional b a;
     val ((lhs, (_, raw_th)), lthy2) = lthy
       |> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
 
@@ -268,32 +269,29 @@
         (member (op =) (Term.add_frees lhs' [])) [(x, T)];
   in ((lhs, (def_name, th')), lthy4) end;
 
-val definition' = gen_def check_spec;
-fun definition xs As B = definition' xs As B false;
-val definition_cmd = gen_def read_spec;
+val definition' = gen_def check_spec_open (K I);
+fun definition xs ys As B = definition' xs ys As B false;
+val definition_cmd = gen_def read_spec_open Attrib.check_src;
 
 
 (* abbreviation *)
 
-fun gen_abbrev prep mode raw_var raw_prop int lthy =
+fun gen_abbrev prep_spec mode raw_var raw_params raw_spec int lthy =
   let
-    val lthy1 = lthy
-      |> Proof_Context.set_syntax_mode mode;
-    val (((vars, (_, prop)), get_pos), _) =
-      prep (the_list raw_var) [] (Attrib.empty_binding, raw_prop)
-        (lthy1 |> Proof_Context.set_mode Proof_Context.mode_abbrev);
-    val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 prop));
+    val lthy1 = lthy |> Proof_Context.set_syntax_mode mode;
+    val ((vars, xs, get_pos, spec), spec_ctxt) = lthy
+      |> Proof_Context.set_mode Proof_Context.mode_abbrev
+      |> prep_spec (the_list raw_var) raw_params [] raw_spec;
+    val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 spec));
     val _ = Name.reject_internal (x, []);
     val (b, mx) =
-      (case vars of
-        [] => (Binding.make (x, get_pos x), NoSyn)
-      | [((b, _), mx)] =>
-          let
-            val y = Variable.check_name b;
-            val _ = x = y orelse
-              error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
-                Position.here (Binding.pos_of b));
-          in (b, mx) end);
+      (case (vars, xs) of
+        ([], []) => (Binding.make (x, get_pos x), NoSyn)
+      | ([(b, _, mx)], [y]) =>
+          if x = y then (b, mx)
+          else
+            error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
+              Position.here (Binding.pos_of b)));
     val lthy2 = lthy1
       |> Local_Theory.abbrev mode ((b, mx), rhs) |> snd
       |> Proof_Context.restore_syntax_mode lthy;
@@ -301,8 +299,8 @@
     val _ = Proof_Display.print_consts int (Position.thread_data ()) lthy2 (K false) [(x, T)];
   in lthy2 end;
 
-val abbreviation = gen_abbrev check_spec;
-val abbreviation_cmd = gen_abbrev read_spec;
+val abbreviation = gen_abbrev check_spec_open;
+val abbreviation_cmd = gen_abbrev read_spec_open;
 
 
 (* notation *)
diff -r d191892b1c23 -r dd6cd88cebd9 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun May 29 14:43:18 2016 +0200
+++ b/src/Pure/Pure.thy	Mon May 30 20:58:54 2016 +0200
@@ -343,19 +343,24 @@
 
 val _ =
   Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
-    (Scan.option Parse_Spec.constdecl -- Parse_Spec.spec
-      >> (fn (a, (b, c)) => #2 oo Specification.definition_cmd a b c));
+    (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) --
+      Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) =>
+        #2 oo Specification.definition_cmd decl params prems spec));
 
 val _ =
   Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
-    (Parse.syntax_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
-      >> (fn (mode, (a, b)) => Specification.abbreviation_cmd mode a b));
+    (Parse.syntax_mode -- Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes
+      >> (fn (((mode, decl), spec), params) => Specification.abbreviation_cmd mode decl params spec));
+
+val axiomatization =
+  Parse.and_list1 (Parse_Spec.thm_name ":" -- Parse.prop) --
+  Parse_Spec.if_assumes -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a));
 
 val _ =
   Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
     (Scan.optional Parse.fixes [] --
-      Scan.optional (Parse.where_ |-- Parse.!!! Parse_Spec.specification) ([], [])
-      >> (fn (a, (b, c)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c)));
+      Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], [])
+      >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d)));
 
 in end\<close>
 
diff -r d191892b1c23 -r dd6cd88cebd9 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Sun May 29 14:43:18 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML	Mon May 30 20:58:54 2016 +0200
@@ -549,7 +549,7 @@
 fun add_definiendum (ml_name, (b, T)) thy =
   thy
   |> Code_Target.add_reserved target ml_name
-  |> Specification.axiomatization [(b, SOME T, NoSyn)] [] []
+  |> Specification.axiomatization [(b, SOME T, NoSyn)] [] [] []
   |-> (fn ([Const (const, _)], _) =>
     Code_Target.set_printings (Constant (const,
       [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))