# HG changeset patch
# User wenzelm
# Date 1461829391 -7200
# Node ID 2f18172214c8b049471f124929f771d086a4b162
# Parent  c9605a284fbad83283503938281ec45a159e3fc5
support 'assumes' in specifications, e.g. 'definition', 'inductive';
tuned signatures;

diff -r c9605a284fba -r 2f18172214c8 src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -175,8 +175,8 @@
       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,
-          ((Binding.prefix_name "below_" (Thm.def_binding name), []), below_eqn))
+      |> 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
     val thy = lthy
diff -r c9605a284fba -r 2f18172214c8 src/HOL/HOLCF/Tools/domaindef.ML
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Thu Apr 28 09:43:11 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 c9605a284fba -r 2f18172214c8 src/HOL/HOLCF/Tools/fixrec.ML
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Thu Apr 28 09:43:11 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 raw_spec lthy)
+          fst (prep_spec raw_fixes (map (rpair []) raw_spec) lthy)
     val names = map (Binding.name_of o fst o fst) fixes
     fun check_head name =
         member (op =) names name orelse
@@ -377,8 +377,8 @@
 
 in
 
-val add_fixrec = gen_fixrec Specification.check_spec
-val add_fixrec_cmd = gen_fixrec Specification.read_spec
+val add_fixrec = gen_fixrec Specification.check_multi_specs
+val add_fixrec_cmd = gen_fixrec Specification.read_multi_specs
 
 end (* local *)
 
@@ -394,13 +394,13 @@
 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 =
+val multi_specs' : (bool * (Attrib.binding * string)) list parser =
   let val unexpected = Scan.ahead (Parse.name || @{keyword "["} || @{keyword "("})
   in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! @{keyword "|"})) end
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword fixrec} "define recursive functions (HOLCF)"
-    (Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs')
+    (Parse.fixes -- (Parse.where_ |-- Parse.!!! multi_specs')
       >> (fn (fixes, specs) => add_fixrec_cmd fixes specs))
 
 end
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Apr 28 09:43:11 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)]
-          [(Attrib.empty_binding, def1), (Attrib.empty_binding, def2)] ||>
+          (map (fn def => ((Attrib.empty_binding, def), [])) [def1, def2]) ||>
         Sign.parent_path
       end) ak_names_types thy3;
     
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -251,11 +251,11 @@
               else Const (@{const_name Nominal.perm}, permT --> T --> T) $ pi $ x
             end;
         in
-          (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
+          ((Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
             (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 c9605a284fba -r 2f18172214c8 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -11,11 +11,11 @@
   val primrec: term list option -> term option ->
     (binding * typ option * mixfix) list ->
     (binding * typ option * mixfix) list ->
-    (Attrib.binding * term) list -> local_theory -> Proof.state
+    Specification.multi_specs -> local_theory -> Proof.state
   val primrec_cmd: string list option -> string option ->
     (binding * string option * mixfix) list ->
     (binding * string option * mixfix) list ->
-    (Attrib.binding * string) list -> local_theory -> Proof.state
+    Specification.multi_specs_cmd -> local_theory -> Proof.state
 end;
 
 structure NominalPrimrec : NOMINAL_PRIMREC =
@@ -380,8 +380,8 @@
 
 in
 
-val primrec = gen_primrec Specification.check_spec (K I);
-val primrec_cmd = gen_primrec Specification.read_spec Syntax.read_term;
+val primrec = gen_primrec Specification.check_multi_specs (K I);
+val primrec_cmd = gen_primrec Specification.read_multi_specs Syntax.read_term;
 
 end;
 
@@ -403,7 +403,7 @@
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_keyword nominal_primrec}
     "define primitive recursive functions on nominal datatypes"
-    (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs
+    (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_multi_specs
       >> (fn ((((invs, fctxt), fixes), params), specs) =>
         primrec_cmd invs fctxt fixes params specs));
 
diff -r c9605a284fba -r 2f18172214c8 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -1020,8 +1020,8 @@
             "\ndoes not match type " ^ ty' ^ " in definition");
         val id' = mk_rulename id;
         val ((t', (_, th)), lthy') = Named_Target.theory_init thy
-          |> Specification.definition
-            (NONE, ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t))));
+          |> Specification.definition NONE []
+            ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t)));
         val phi =
           Proof_Context.export_morphism lthy'
             (Proof_Context.init_global (Proof_Context.theory_of lthy'));
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/BNF/bnf_axiomatization.ML
--- a/src/HOL/Tools/BNF/bnf_axiomatization.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_axiomatization.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -82,7 +82,7 @@
     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;
+      (Specification.axiomatization [] [] [((mk_b "axioms" Binding.empty, []), flat all_goalss)]) lthy;
 
     fun mk_wit_thms set_maps =
       Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals)
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/BNF/bnf_gfp_grec.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Thu Apr 28 09:43:11 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 (pair Attrib.empty_binding) 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 c9605a284fba -r 2f18172214c8 src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -1829,7 +1829,7 @@
 
     val ({defname, pelims = [[pelim]], pinducts = [pinduct], psimps = [psimp], ...}, lthy) =
       Function.add_function [(Binding.concealed binding, NONE, NoSyn)]
-        [(apfst Binding.concealed Attrib.empty_binding, 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_spec 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 c9605a284fba -r 2f18172214c8 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -1587,7 +1587,8 @@
 
     val (raw_specs, of_specs_opt) =
       split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy));
-    val (fixes, specs) = fst (Specification.read_spec raw_fixes raw_specs lthy);
+    val (fixes, specs) =
+      fst (Specification.read_multi_specs raw_fixes (map (rpair []) raw_specs) lthy);
   in
     primcorec_ursive auto opts fixes specs of_specs_opt lthy
   end;
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -26,12 +26,12 @@
   val datatype_compat_global: string list -> theory -> theory
   val datatype_compat_cmd: string list -> local_theory -> local_theory
   val add_datatype: preference list -> Old_Datatype_Aux.spec list -> theory -> string list * theory
-  val primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
+  val primrec: (binding * typ option * mixfix) list -> Specification.multi_specs ->
     local_theory -> (term list * thm list) * local_theory
   val primrec_global: (binding * typ option * mixfix) list ->
-    (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
+    Specification.multi_specs -> theory -> (term list * thm list) * theory
   val primrec_overloaded: (string * (string * typ) * bool) list ->
-    (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> theory ->
+    (binding * typ option * mixfix) list -> Specification.multi_specs -> theory ->
     (term list * thm list) * theory
   val primrec_simple: ((binding * typ) * mixfix) list -> term list ->
     local_theory -> (string list * (term list * thm list)) * local_theory
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -62,16 +62,16 @@
   val lfp_rec_sugar_interpretation: string ->
     (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory
 
-  val primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
+  val primrec: (binding * typ option * mixfix) list -> Specification.multi_specs ->
     local_theory -> (term list * thm list * thm list list) * local_theory
   val primrec_cmd: rec_option list -> (binding * string option * mixfix) list ->
-    (Attrib.binding * string) list -> local_theory ->
+    Specification.multi_specs_cmd -> local_theory ->
     (term list * thm list * thm list list) * local_theory
   val primrec_global: (binding * typ option * mixfix) list ->
-    (Attrib.binding * term) list -> theory -> (term list * thm list * thm list list) * theory
+    Specification.multi_specs -> theory -> (term list * thm list * thm list list) * theory
   val primrec_overloaded: (string * (string * typ) * bool) list ->
     (binding * typ option * mixfix) list ->
-    (Attrib.binding * term) list -> theory -> (term list * thm list * thm list list) * theory
+    Specification.multi_specs -> theory -> (term list * thm list * thm list list) * theory
   val primrec_simple: ((binding * typ) * mixfix) list -> term list -> local_theory ->
     ((string list * (binding -> binding) list) *
     (term list * thm list * (int list list * thm list list))) * local_theory
@@ -666,8 +666,8 @@
     old_primrec raw_fixes raw_specs lthy
     |>> (fn (ts, thms) => (ts, [], [thms]));
 
-val primrec = gen_primrec Old_Primrec.primrec Specification.check_spec [];
-val primrec_cmd = gen_primrec Old_Primrec.primrec_cmd Specification.read_spec;
+val primrec = gen_primrec Old_Primrec.primrec Specification.check_multi_specs [];
+val primrec_cmd = gen_primrec Old_Primrec.primrec_cmd Specification.read_multi_specs;
 
 fun primrec_global fixes specs =
   Named_Target.theory_init
@@ -688,7 +688,7 @@
   "define primitive recursive functions"
   ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser)
       --| @{keyword ")"}) []) --
-    (Parse.fixes -- Parse_Spec.where_alt_specs)
+    (Parse.fixes -- Parse_Spec.where_multi_specs)
     >> (fn (opts, (fixes, specs)) => snd o primrec_cmd opts fixes specs));
 
 end;
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -623,12 +623,12 @@
                 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),
-                    ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd)
+                  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),
-                ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos
+              Specification.definition (SOME (b, NONE, NoSyn)) []
+                ((Thm.def_binding b, []), sel_spec b proto_sels) #>> apsnd snd) sel_infos
             ||> `Local_Theory.close_target;
 
           val phi = Proof_Context.export_morphism lthy lthy';
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Thu Apr 28 09:43:11 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 c9605a284fba -r 2f18172214c8 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Function/fun.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -9,10 +9,10 @@
 sig
   val fun_config : Function_Common.function_config
   val add_fun : (binding * typ option * mixfix) list ->
-    (Attrib.binding * term) list -> Function_Common.function_config ->
+    Specification.multi_specs -> Function_Common.function_config ->
     local_theory -> Proof.context
   val add_fun_cmd : (binding * string option * mixfix) list ->
-    (Attrib.binding * string) list -> Function_Common.function_config ->
+    Specification.multi_specs_cmd -> Function_Common.function_config ->
     bool -> local_theory -> Proof.context
 end
 
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/Function/fun_cases.ML
--- a/src/HOL/Tools/Function/fun_cases.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Function/fun_cases.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -56,7 +56,7 @@
 val _ =
   Outer_Syntax.local_theory @{command_keyword fun_cases}
     "create simplified instances of elimination rules for function equations"
-    (Parse.and_list1 Parse_Spec.specs >> (snd oo fun_cases_cmd));
+    (Parse.and_list1 Parse_Spec.simple_specs >> (snd oo fun_cases_cmd));
 
 end;
 
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Function/function.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -9,19 +9,19 @@
   include FUNCTION_DATA
 
   val add_function: (binding * typ option * mixfix) list ->
-    (Attrib.binding * term) list -> Function_Common.function_config ->
+    Specification.multi_specs -> Function_Common.function_config ->
     (Proof.context -> tactic) -> local_theory -> info * local_theory
 
   val add_function_cmd: (binding * string option * mixfix) list ->
-    (Attrib.binding * string) list -> Function_Common.function_config ->
+    Specification.multi_specs_cmd -> Function_Common.function_config ->
     (Proof.context -> tactic) -> bool -> local_theory -> info * local_theory
 
   val function: (binding * typ option * mixfix) list ->
-    (Attrib.binding * term) list -> Function_Common.function_config ->
+    Specification.multi_specs -> Function_Common.function_config ->
     local_theory -> Proof.state
 
   val function_cmd: (binding * string option * mixfix) list ->
-    (Attrib.binding * string) list -> Function_Common.function_config ->
+    Specification.multi_specs_cmd -> Function_Common.function_config ->
     bool -> local_theory -> Proof.state
 
   val prove_termination: term option -> tactic -> local_theory ->
@@ -149,8 +149,8 @@
     |> afterqed [[pattern_thm]]
   end
 
-val add_function = gen_add_function false Specification.check_spec
-fun add_function_cmd a b c d int = gen_add_function int Specification.read_spec a b c d
+val add_function = gen_add_function false Specification.check_multi_specs
+fun add_function_cmd a b c d int = gen_add_function int Specification.read_multi_specs a b c d
 
 fun gen_function do_print prep fixspec eqns config lthy =
   let
@@ -162,8 +162,8 @@
     |> Proof.refine_singleton (Method.primitive_text (K (K goal_state)))
   end
 
-val function = gen_function false Specification.check_spec
-fun function_cmd a b c int = gen_function int Specification.read_spec a b c
+val function = gen_function false Specification.check_multi_specs
+fun function_cmd a b c int = gen_function int Specification.read_multi_specs a b c
 
 fun prepare_termination_proof prep_term raw_term_opt lthy =
   let
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -100,7 +100,7 @@
   val default_config : function_config
   val function_parser : function_config ->
     ((function_config * (binding * string option * mixfix) list) *
-      (Attrib.binding * string) list) parser
+      Specification.multi_specs_cmd) parser
 end
 
 structure Function_Common : FUNCTION_COMMON =
@@ -374,7 +374,7 @@
      >> (fn opts => fold apply_opt opts default)
 in
   fun function_parser default_cfg =
-      config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs
+      config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_multi_specs
 end
 
 
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Thu Apr 28 09:43:11 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;
@@ -306,14 +306,14 @@
     |> note_qualified ("fixp_induct", [specialized_fixp_induct])
   end;
 
-val add_partial_function = gen_add_partial_function Specification.check_spec;
-val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;
+val add_partial_function = gen_add_partial_function Specification.check_multi_specs;
+val add_partial_function_cmd = gen_add_partial_function Specification.read_multi_specs;
 
 val mode = @{keyword "("} |-- Parse.name --| @{keyword ")"};
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function"
-    ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
+    ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.simple_spec)))
       >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
 
 end;
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -89,8 +89,8 @@
     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)), 
-        ((Binding.empty, []), definition_term)) lthy |>> (snd #> snd);
+      Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) []
+        ((Binding.empty, []), definition_term) lthy |>> (snd #> snd);
     fun raw_def lthy =
       let
         val ((_, rhs), prove) = Local_Defs.derived_def lthy {conditional = true} definition_term;
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/Old_Datatype/old_primrec.ML
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -9,14 +9,14 @@
 signature OLD_PRIMREC =
 sig
   val primrec: (binding * typ option * mixfix) list ->
-    (Attrib.binding * term) list -> local_theory -> (term list * thm list) * local_theory
+    Specification.multi_specs -> local_theory -> (term list * thm list) * local_theory
   val primrec_cmd: (binding * string option * mixfix) list ->
-    (Attrib.binding * string) list -> local_theory -> (term list * thm list) * local_theory
+    Specification.multi_specs_cmd -> local_theory -> (term list * thm list) * local_theory
   val primrec_global: (binding * typ option * mixfix) list ->
-    (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
+    Specification.multi_specs -> theory -> (term list * thm list) * theory
   val primrec_overloaded: (string * (string * typ) * bool) list ->
     (binding * typ option * mixfix) list ->
-    (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
+    Specification.multi_specs -> theory -> (term list * thm list) * theory
   val primrec_simple: ((binding * typ) * mixfix) list -> term list ->
     local_theory -> (string * (term list * thm list)) * local_theory
 end;
@@ -290,8 +290,8 @@
 
 in
 
-val primrec = gen_primrec Specification.check_spec;
-val primrec_cmd = gen_primrec Specification.read_spec;
+val primrec = gen_primrec Specification.check_multi_specs;
+val primrec_cmd = gen_primrec Specification.read_multi_specs;
 
 end;
 
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Apr 28 09:43:11 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 c9605a284fba -r 2f18172214c8 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -365,7 +365,7 @@
       Function.add_function
         (map (fn (name, T) => (Binding.concealed (Binding.name name), SOME T, NoSyn))
           (names ~~ Ts))
-        (map (pair (apfst Binding.concealed Attrib.empty_binding)) 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 c9605a284fba -r 2f18172214c8 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -266,8 +266,8 @@
     |> 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, (apfst Binding.concealed
-            Attrib.empty_binding, random_def))) random_defs')
+          Specification.definition NONE []
+            ((Binding.concealed Binding.empty, []), random_def)) random_defs')
     |> snd
     |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   end;
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Thu Apr 28 09:43:11 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 c9605a284fba -r 2f18172214c8 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/inductive.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -54,7 +54,7 @@
   val add_inductive: bool -> bool ->
     (binding * string option * mixfix) list ->
     (binding * string option * mixfix) list ->
-    (Attrib.binding * string) list ->
+    Specification.multi_specs_cmd ->
     (Facts.ref * Token.src list) list ->
     local_theory -> inductive_result * local_theory
   val add_inductive_global: inductive_flags ->
@@ -88,7 +88,7 @@
   val gen_add_inductive: add_ind_def -> bool -> bool ->
     (binding * string option * mixfix) list ->
     (binding * string option * mixfix) list ->
-    (Attrib.binding * string) list -> (Facts.ref * Token.src list) list ->
+    Specification.multi_specs_cmd -> (Facts.ref * Token.src list) list ->
     local_theory -> inductive_result * local_theory
   val gen_ind_decl: add_ind_def -> bool -> (local_theory -> local_theory) parser
 end;
@@ -1084,7 +1084,7 @@
   let
     val ((vars, intrs), _) = lthy
       |> Proof_Context.set_mode Proof_Context.mode_abbrev
-      |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
+      |> Specification.read_multi_specs (cnames_syn @ pnames_syn) intro_srcs;
     val (cs, ps) = chop (length cnames_syn) vars;
     val monos = Attrib.eval_thms lthy raw_monos;
     val flags =
@@ -1170,7 +1170,7 @@
 
 fun gen_ind_decl mk_def coind =
   Parse.fixes -- Parse.for_fixes --
-  Scan.optional Parse_Spec.where_alt_specs [] --
+  Scan.optional Parse_Spec.where_multi_specs [] --
   Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.thms1) []
   >> (fn (((preds, params), specs), monos) =>
       (snd o gen_add_inductive mk_def true coind preds params specs monos));
@@ -1188,12 +1188,12 @@
 val _ =
   Outer_Syntax.local_theory @{command_keyword inductive_cases}
     "create simplified instances of elimination rules"
-    (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
+    (Parse.and_list1 Parse_Spec.simple_specs >> (snd oo inductive_cases));
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword inductive_simps}
     "create simplification rules for inductive predicates"
-    (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
+    (Parse.and_list1 Parse_Spec.simple_specs >> (snd oo inductive_simps));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_inductives}
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -20,7 +20,7 @@
   val add_inductive: bool -> bool ->
     (binding * string option * mixfix) list ->
     (binding * string option * mixfix) list ->
-    (Attrib.binding * string) list -> (Facts.ref * Token.src list) list ->
+    Specification.multi_specs_cmd -> (Facts.ref * Token.src list) list ->
     local_theory -> Inductive.inductive_result * local_theory
   val mono_add: attribute
   val mono_del: attribute
diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/record.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -1734,7 +1734,7 @@
     thy
     |> Class.instantiation ([tyco], vs, sort)
     |> `(fn lthy => Syntax.check_term lthy eq)
-    |-> (fn eq => Specification.definition (NONE, (apfst Binding.concealed Attrib.empty_binding, 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,8 +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 c9605a284fba -r 2f18172214c8 src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Typerep.thy	Thu Apr 28 09:43:11 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 c9605a284fba -r 2f18172214c8 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -8,13 +8,15 @@
 sig
   val thm_name: string -> Attrib.binding parser
   val opt_thm_name: string -> Attrib.binding parser
-  val spec: (Attrib.binding * string) parser
-  val specs: (Attrib.binding * string list) parser
-  val alt_specs: (Attrib.binding * string) list parser
-  val where_alt_specs: (Attrib.binding * string) list parser
   val name_facts: (Attrib.binding * (Facts.ref * Token.src list) list) list parser
+  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 constdecl: (binding * string option * mixfix) parser
-  val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
   val includes: (xstring * Position.T) list parser
   val locale_fixes: (binding * string option * mixfix) list parser
   val locale_insts: (string option list * (Attrib.binding * string) list) parser
@@ -37,7 +39,7 @@
 structure Parse_Spec: PARSE_SPEC =
 struct
 
-(* theorem specifications *)
+(* simple specifications *)
 
 fun thm_name s = Parse.binding -- Parse.opt_attribs --| Parse.$$$ s;
 
@@ -46,18 +48,31 @@
     ((Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) --| Parse.$$$ s)
     Attrib.empty_binding;
 
-val spec = opt_thm_name ":" -- Parse.prop;
-val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
-
-val alt_specs =
-  Parse.enum1 "|"
-    (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
-
-val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
+val simple_spec = opt_thm_name ":" -- Parse.prop;
+val simple_specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
 
 val name_facts = Parse.and_list1 (opt_thm_name "=" -- Parse.thms1);
 
 
+(* structured specifications *)
+
+val if_assumes =
+  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 --|
+      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;
+
+
 (* basic constant specifications *)
 
 val constdecl =
@@ -67,8 +82,6 @@
       Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
   >> Scan.triple2;
 
-val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
-
 
 (* locale and context elements *)
 
diff -r c9605a284fba -r 2f18172214c8 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -11,45 +11,40 @@
     term list * Proof.context
   val read_prop: string -> (binding * string option * mixfix) list -> Proof.context ->
     term * Proof.context
-  val check_free_spec:
-    (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
-    ((((binding * typ) * mixfix) list * (Attrib.binding * term) list) * (string -> Position.T))
+  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_free_spec:
-    (binding * string option * mixfix) list -> (Attrib.binding * string) list -> Proof.context ->
-    ((((binding * typ) * mixfix) list * (Attrib.binding * term) list) * (string -> Position.T))
+  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
-  val check_spec:
-    (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
+  type multi_specs = ((Attrib.binding * term) * term list) list
+  type multi_specs_cmd = ((Attrib.binding * string) * string 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_spec:
-    (binding * string option * mixfix) list -> (Attrib.binding * string) 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 ->
+  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 ->
+  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 ->
-    (Attrib.binding * term list) list -> theory ->
-    (term list * thm list list) * theory
-  val axiomatization_cmd: (binding * string option * mixfix) list ->
-    (Attrib.binding * string list) list -> theory ->
-    (term list * thm list list) * theory
+  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 axiom: Attrib.binding * term -> theory -> thm * theory
-  val definition:
-    (binding * typ option * mixfix) option * (Attrib.binding * term) ->
-    local_theory -> (term * (string * thm)) * local_theory
-  val definition':
-    (binding * typ option * mixfix) option * (Attrib.binding * term) ->
-    bool -> local_theory -> (term * (string * thm)) * local_theory
-  val definition_cmd:
-    (binding * string option * mixfix) option * (Attrib.binding * string) ->
-    bool -> local_theory -> (term * (string * thm)) * local_theory
-  val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option * term ->
+  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 ->
+  val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option -> 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 ->
@@ -141,7 +136,7 @@
           map (Variable.markup_entity_def params_ctxt ##> Properties.remove Markup.kindN) xs);
 
     val Asss0 =
-      (map o map) snd raw_specss
+      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)
@@ -151,8 +146,8 @@
     val idx = (fold o fold o fold) Term.maxidx_term Asss1 ~1 + 1;
 
     val (Asss2, _) =
-      fold_map (fn Ass => fn i => (burrow (close_forms params_ctxt auto_close i []) Ass, i + 1))
-        Asss1 idx;
+      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;
@@ -160,7 +155,7 @@
     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)) (flat raw_specss);
+      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
@@ -169,45 +164,50 @@
   in (((params, name_atts ~~ specs), get_pos), specs_ctxt) end;
 
 
-fun single_spec (a, prop) = [(a, [prop])];
+fun single_spec ((a, B), As) = ([(a, [B])], As);
 fun the_spec (a, [prop]) = (a, prop);
 
-fun prep_spec prep_var parse_prop prep_att auto_close vars specs =
+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);
 
 in
 
-fun check_free_spec vars specs =
-  prep_spec Proof_Context.cert_var (K I) (K I) false vars specs;
+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;
 
-fun read_free_spec vars specs =
-  prep_spec Proof_Context.read_var Syntax.parse_prop Attrib.check_src false vars specs;
+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;
 
-fun check_spec vars specs =
-  prep_spec Proof_Context.cert_var (K I) (K I) true vars specs #> apfst fst;
+type multi_specs = ((Attrib.binding * term) * term list) list;
+type multi_specs_cmd = ((Attrib.binding * string) * string list) list;
 
-fun read_spec vars specs =
-  prep_spec Proof_Context.read_var Syntax.parse_prop Attrib.check_src true vars specs #> apfst fst;
+fun check_multi_specs xs specs =
+  prep_specs Proof_Context.cert_var (K I) (K I) true xs specs #>> #1;
+
+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 vars specs =
-  prepare Proof_Context.cert_var (K I) (K I) true vars [specs] #> apfst fst
+fun check_specification xs As Bs =
+  prepare Proof_Context.cert_var (K I) (K I) true xs [(Bs, As)] #>> #1;
 
-fun read_specification vars specs =
-  prepare Proof_Context.read_var Syntax.parse_prop Attrib.check_src true vars [specs] #> apfst fst;
+fun read_specification xs As Bs =
+  prepare Proof_Context.read_var Syntax.parse_prop Attrib.check_src true xs [(Bs, As)] #>> #1;
 
 end;
 
 
 (* axiomatization -- within global theory *)
 
-fun gen_axioms prep raw_vars raw_specs thy =
+fun gen_axioms prep raw_decls raw_prems raw_concls thy =
   let
-    val ((vars, specs), _) = prep raw_vars raw_specs (Proof_Context.init_global thy);
-    val xs = map (fn ((b, T), _) => (Variable.check_name b, T)) vars;
+    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;
 
     (*consts*)
-    val (consts, consts_thy) = thy |> fold_map Theory.specify_const vars;
+    val (consts, consts_thy) = thy |> fold_map Theory.specify_const decls;
     val subst = Term.subst_atomic (map Free xs ~~ consts);
 
     (*axioms*)
@@ -228,15 +228,15 @@
 val axiomatization = gen_axioms check_specification;
 val axiomatization_cmd = gen_axioms read_specification;
 
-fun axiom (b, ax) = axiomatization [] [(b, [ax])] #>> (hd o hd o snd);
+fun axiom (b, ax) = axiomatization [] [] [(b, [ax])] #>> (hd o hd o snd);
 
 
 (* definition *)
 
-fun gen_def prep (raw_var, raw_spec) int lthy =
+fun gen_def prep raw_var raw_prems raw_spec int lthy =
   let
-    val ((vars, [((raw_name, atts), prop)]), get_pos) =
-      fst (prep (the_list raw_var) [raw_spec] lthy);
+    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 _ = Name.reject_internal (x, []);
     val (b, mx) =
@@ -266,19 +266,19 @@
         (member (op =) (Term.add_frees lhs' [])) [(x, T)];
   in ((lhs, (def_name, th')), lthy4) end;
 
-val definition' = gen_def check_free_spec;
-fun definition spec = definition' spec false;
-val definition_cmd = gen_def read_free_spec;
+val definition' = gen_def check_spec;
+fun definition xs As B = definition' xs As B false;
+val definition_cmd = gen_def read_spec;
 
 
 (* abbreviation *)
 
-fun gen_abbrev prep mode (raw_var, raw_prop) int lthy =
+fun gen_abbrev prep mode raw_var raw_prop 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)]
+    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 _ = Name.reject_internal (x, []);
@@ -299,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_free_spec;
-val abbreviation_cmd = gen_abbrev read_free_spec;
+val abbreviation = gen_abbrev check_spec;
+val abbreviation_cmd = gen_abbrev read_spec;
 
 
 (* notation *)
diff -r c9605a284fba -r 2f18172214c8 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/Pure/Pure.thy	Thu Apr 28 09:43:11 2016 +0200
@@ -343,18 +343,19 @@
 
 val _ =
   Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
-    (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
+    (Scan.option Parse_Spec.constdecl -- Parse_Spec.spec
+      >> (fn (a, (b, c)) => #2 oo Specification.definition_cmd a b c));
 
 val _ =
   Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
     (Parse.syntax_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
-      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
+      >> (fn (mode, (a, b)) => Specification.abbreviation_cmd mode a b));
 
 val _ =
   Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
     (Scan.optional Parse.fixes [] --
-      Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
-      >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
+      Scan.optional (Parse.where_ |-- Parse.!!! Parse_Spec.specification) ([], [])
+      >> (fn (a, (b, c)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c)));
 
 in end\<close>
 
diff -r c9605a284fba -r 2f18172214c8 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/Pure/ROOT.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -251,9 +251,9 @@
 ML_file "Isar/code.ML";
 
 (*specifications*)
-ML_file "Isar/parse_spec.ML";
 ML_file "Isar/spec_rules.ML";
 ML_file "Isar/specification.ML";
+ML_file "Isar/parse_spec.ML";
 ML_file "Isar/typedecl.ML";
 
 (*toplevel transactions*)
diff -r c9605a284fba -r 2f18172214c8 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -548,7 +548,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)))]))