# HG changeset patch
# User wenzelm
# Date 1464529225 -7200
# Node ID ddfd021884b49443b6b05c9cd4aa5f360be046c5
# Parent  231e261fd6bc9afa967f69e01bea4f97cf067649
clarified check_open_spec / read_open_spec;
allow 'for' fixes in 'abbreviation', 'definition';

diff -r 231e261fd6bc -r ddfd021884b4 NEWS
--- a/NEWS	Sat May 28 23:55:41 2016 +0200
+++ b/NEWS	Sun May 29 15:40:25 2016 +0200
@@ -66,14 +66,14 @@
 
 *** 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
 traditional long statement form (in prefix). Local premises are called
diff -r 231e261fd6bc -r ddfd021884b4 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Sat May 28 23:55:41 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Sun May 29 15:40:25 2016 +0200
@@ -285,14 +285,19 @@
   ``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} prems @{syntax for_fixes}
+    ;
+    prems: (@'if' ((@{syntax prop}+) + @'and'))?
+    ;
+    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
diff -r 231e261fd6bc -r ddfd021884b4 src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Sun May 29 15:40:25 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 231e261fd6bc -r ddfd021884b4 src/HOL/HOLCF/Tools/domaindef.ML
--- a/src/HOL/HOLCF/Tools/domaindef.ML	Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Sun May 29 15:40:25 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 231e261fd6bc -r ddfd021884b4 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sun May 29 15:40:25 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 231e261fd6bc -r ddfd021884b4 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun May 29 15:40:25 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 231e261fd6bc -r ddfd021884b4 src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML	Sun May 29 15:40:25 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 231e261fd6bc -r ddfd021884b4 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sun May 29 15:40:25 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 231e261fd6bc -r ddfd021884b4 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun May 29 15:40:25 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 231e261fd6bc -r ddfd021884b4 src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Sun May 29 15:40:25 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 231e261fd6bc -r ddfd021884b4 src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Sun May 29 15:40:25 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 231e261fd6bc -r ddfd021884b4 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/inductive.ML	Sun May 29 15:40:25 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 231e261fd6bc -r ddfd021884b4 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/record.ML	Sun May 29 15:40:25 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 231e261fd6bc -r ddfd021884b4 src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Typerep.thy	Sun May 29 15:40:25 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 231e261fd6bc -r ddfd021884b4 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Sat May 28 23:55:41 2016 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Sun May 29 15:40:25 2016 +0200
@@ -12,7 +12,6 @@
   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 constdecl: (binding * string option * mixfix) parser
@@ -59,8 +58,6 @@
   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 --|
diff -r 231e261fd6bc -r ddfd021884b4 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat May 28 23:55:41 2016 +0200
+++ b/src/Pure/Isar/specification.ML	Sun May 29 15:40:25 2016 +0200
@@ -11,14 +11,14 @@
     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
+  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) list
   type multi_specs_cmd = ((Attrib.binding * string) * string list) list
   val check_multi_specs: (binding * typ option * mixfix) list -> multi_specs -> Proof.context ->
@@ -32,16 +32,19 @@
     (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
@@ -96,14 +99,30 @@
 
 local
 
-fun close_form ctxt auto_close prems concl =
-  if not auto_close andalso null prems then concl
-  else
-    let
-      val xs =
-        if auto_close then rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) [])
-        else [];
-    in Logic.close_prop_constraint (Variable.default_type ctxt) (xs ~~ xs) prems concl 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 prems concl =
+  let val xs = rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) []);
+  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
@@ -118,60 +137,58 @@
       | get _ _ = [];
   in get [] end;
 
-fun prep_specs 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;
+
+    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 propss0 =
       map (fn ((_, raw_concl), raw_prems) => raw_concl :: raw_prems) raw_specss
-      |> burrow (grouped 10 Par_List.map_independent (parse_prop params_ctxt));
-    val names =
-      Variable.names_of (params_ctxt |> (fold o fold) Variable.declare_term propss0)
-      |> fold Name.declare xs;
+      |> burrow (grouped 10 Par_List.map_independent (parse_prop vars_ctxt));
     val props =
-      (fold_map o fold_map) Term.free_dummy_patterns propss0 names
-      |> fst |> map (fn concl :: prems => close_form params_ctxt auto_close prems concl);
+      dummy_frees vars_ctxt xs propss0
+      |> map (fn concl :: prems => close_form vars_ctxt prems concl);
 
-    val specs = Syntax.check_props params_ctxt props;
-    val specs_ctxt = params_ctxt |> 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)) (map #1 raw_specss);
-
-    fun get_pos x =
-      (case maps (get_positions specs_ctxt x) props of
-        [] => Position.none
-      | pos :: _ => pos);
-  in (((params, name_atts ~~ specs), get_pos), specs_ctxt) end;
+  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;
-
-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;
+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;
 
 type multi_specs = ((Attrib.binding * term) * term list) list;
 type multi_specs_cmd = ((Attrib.binding * string) * string 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;
+  prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src xs specs;
 
 end;
 
@@ -219,23 +236,23 @@
 
 (* 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));
 
@@ -252,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;
@@ -285,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 231e261fd6bc -r ddfd021884b4 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sat May 28 23:55:41 2016 +0200
+++ b/src/Pure/Pure.thy	Sun May 29 15:40:25 2016 +0200
@@ -343,13 +343,14 @@
 
 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) --