type Attrib.binding abbreviates Name.binding without attributes;
authorwenzelm
Tue Sep 02 16:55:33 2008 +0200 (2008-09-02)
changeset 28084a05ca48ef263
parent 28083 103d9282a946
child 28085 914183e229e9
type Attrib.binding abbreviates Name.binding without attributes;
Attrib.no_binding refers to Name.no_binding;
src/HOL/Library/Eval.thy
src/HOL/Library/RType.thy
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/inductive_wrap.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_set_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/typecopy_package.ML
src/HOL/Typedef.thy
src/HOL/ex/Quickcheck.thy
src/HOLCF/Tools/fixrec_package.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/class.ML
src/Pure/Isar/constdefs.ML
src/Pure/Isar/element.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/spec_parse.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/theory_target.ML
src/ZF/Tools/ind_cases.ML
     1.1 --- a/src/HOL/Library/Eval.thy	Tue Sep 02 14:10:45 2008 +0200
     1.2 +++ b/src/HOL/Library/Eval.thy	Tue Sep 02 16:55:33 2008 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4        thy
     1.5        |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
     1.6        |> `(fn lthy => Syntax.check_term lthy eq)
     1.7 -      |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
     1.8 +      |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
     1.9        |> snd
    1.10        |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    1.11        |> LocalTheory.exit
     2.1 --- a/src/HOL/Library/RType.thy	Tue Sep 02 14:10:45 2008 +0200
     2.2 +++ b/src/HOL/Library/RType.thy	Tue Sep 02 16:55:33 2008 +0200
     2.3 @@ -67,7 +67,7 @@
     2.4      thy
     2.5      |> TheoryTarget.instantiation ([tyco], vs, @{sort rtype})
     2.6      |> `(fn lthy => Syntax.check_term lthy eq)
     2.7 -    |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
     2.8 +    |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
     2.9      |> snd
    2.10      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    2.11      |> LocalTheory.exit
     3.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Sep 02 14:10:45 2008 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_package.ML	Tue Sep 02 16:55:33 2008 +0200
     3.3 @@ -286,7 +286,7 @@
     3.4                else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
     3.5              end;
     3.6          in
     3.7 -          ((Name.no_binding, []), HOLogic.mk_Trueprop (HOLogic.mk_eq
     3.8 +          (Attrib.no_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
     3.9              (Free (nth perm_names_types' i) $
    3.10                 Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
    3.11                 list_comb (c, args),
    3.12 @@ -563,7 +563,7 @@
    3.13             skip_mono = true}
    3.14            (map (fn (s, T) => ((Name.binding s, T --> HOLogic.boolT), NoSyn))
    3.15               (rep_set_names' ~~ recTs'))
    3.16 -          [] (map (fn x => ((Name.no_binding, []), x)) intr_ts) [] thy3;
    3.17 +          [] (map (fn x => (Attrib.no_binding, x)) intr_ts) [] thy3;
    3.18  
    3.19      (**** Prove that representing set is closed under permutation ****)
    3.20  
    3.21 @@ -1480,7 +1480,7 @@
    3.22             skip_mono = true}
    3.23            (map (fn (s, T) => ((Name.binding s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    3.24            (map dest_Free rec_fns)
    3.25 -          (map (fn x => ((Name.no_binding, []), x)) rec_intr_ts) [] ||>
    3.26 +          (map (fn x => (Attrib.no_binding, x)) rec_intr_ts) [] ||>
    3.27        PureThy.hide_fact true (NameSpace.append (Sign.full_name thy10 big_rec_name) "induct");
    3.28  
    3.29      (** equivariance **)
     4.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Sep 02 14:10:45 2008 +0200
     4.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Sep 02 16:55:33 2008 +0200
     4.3 @@ -160,7 +160,7 @@
     4.4              skip_mono = true}
     4.5            (map (fn (s, T) => ((Name.binding s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
     4.6            (map dest_Free rec_fns)
     4.7 -          (map (fn x => ((Name.no_binding, []), x)) rec_intr_ts) [] thy0;
     4.8 +          (map (fn x => (Attrib.no_binding, x)) rec_intr_ts) [] thy0;
     4.9  
    4.10      (* prove uniqueness and termination of primrec combinators *)
    4.11  
     5.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Sep 02 14:10:45 2008 +0200
     5.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Sep 02 16:55:33 2008 +0200
     5.3 @@ -442,7 +442,7 @@
     5.4            (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
     5.5          val def' = Syntax.check_term lthy def;
     5.6          val ((_, (_, thm)), lthy') = Specification.definition
     5.7 -          (NONE, ((Name.no_binding, []), def')) lthy;
     5.8 +          (NONE, (Attrib.no_binding, def')) lthy;
     5.9          val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
    5.10          val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
    5.11        in (thm', lthy') end;
     6.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Sep 02 14:10:45 2008 +0200
     6.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Sep 02 16:55:33 2008 +0200
     6.3 @@ -187,7 +187,7 @@
     6.4             alt_name = Name.binding big_rec_name, coind = false, no_elim = true, no_ind = false,
     6.5             skip_mono = true}
     6.6            (map (fn s => ((Name.binding s, UnivT'), NoSyn)) rep_set_names') []
     6.7 -          (map (fn x => ((Name.no_binding, []), x)) intr_ts) [] thy1;
     6.8 +          (map (fn x => (Attrib.no_binding, x)) intr_ts) [] thy1;
     6.9  
    6.10      (********************************* typedef ********************************)
    6.11  
     7.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Sep 02 14:10:45 2008 +0200
     7.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Sep 02 16:55:33 2008 +0200
     7.3 @@ -10,14 +10,14 @@
     7.4  signature FUNDEF_PACKAGE =
     7.5  sig
     7.6      val add_fundef :  (Name.binding * string option * mixfix) list
     7.7 -                      -> ((Name.binding * Attrib.src list) * string) list 
     7.8 +                      -> (Attrib.binding * string) list 
     7.9                        -> FundefCommon.fundef_config
    7.10                        -> bool list
    7.11                        -> local_theory
    7.12                        -> Proof.state
    7.13  
    7.14      val add_fundef_i:  (Name.binding * typ option * mixfix) list
    7.15 -                       -> ((Name.binding * Attrib.src list) * term) list
    7.16 +                       -> (Attrib.binding * term) list
    7.17                         -> FundefCommon.fundef_config
    7.18                         -> bool list
    7.19                         -> local_theory
     8.1 --- a/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Sep 02 14:10:45 2008 +0200
     8.2 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Sep 02 16:55:33 2008 +0200
     8.3 @@ -51,7 +51,7 @@
     8.4                skip_mono = true}
     8.5              [((Name.binding R, T), NoSyn)] (* the relation *)
     8.6              [] (* no parameters *)
     8.7 -            (map (fn t => ((Name.no_binding, []), t)) defs) (* the intros *)
     8.8 +            (map (fn t => (Attrib.no_binding, t)) defs) (* the intros *)
     8.9              [] (* no special monos *)
    8.10              lthy
    8.11  
     9.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Sep 02 14:10:45 2008 +0200
     9.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Sep 02 16:55:33 2008 +0200
     9.3 @@ -33,25 +33,24 @@
     9.4    val inductive_forall_name: string
     9.5    val inductive_forall_def: thm
     9.6    val rulify: thm -> thm
     9.7 -  val inductive_cases: ((Name.binding * Attrib.src list) * string list) list ->
     9.8 -    Proof.context -> thm list list * local_theory
     9.9 -  val inductive_cases_i: ((Name.binding * Attrib.src list) * term list) list ->
    9.10 -    Proof.context -> thm list list * local_theory
    9.11 +  val inductive_cases: (Attrib.binding * string list) list -> Proof.context ->
    9.12 +    thm list list * local_theory
    9.13 +  val inductive_cases_i: (Attrib.binding * term list) list -> Proof.context ->
    9.14 +    thm list list * local_theory
    9.15    type inductive_flags
    9.16    val add_inductive_i:
    9.17      inductive_flags -> ((Name.binding * typ) * mixfix) list ->
    9.18 -    (string * typ) list -> ((Name.binding * Attrib.src list) * term) list -> thm list ->
    9.19 -      local_theory -> inductive_result * local_theory
    9.20 +    (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
    9.21 +    inductive_result * local_theory
    9.22    val add_inductive: bool -> bool ->
    9.23      (Name.binding * string option * mixfix) list ->
    9.24      (Name.binding * string option * mixfix) list ->
    9.25 -    ((Name.binding * Attrib.src list) * string) list ->
    9.26 +    (Attrib.binding * string) list ->
    9.27      (Facts.ref * Attrib.src list) list ->
    9.28      local_theory -> inductive_result * local_theory
    9.29    val add_inductive_global: string -> inductive_flags ->
    9.30 -    ((Name.binding * typ) * mixfix) list ->
    9.31 -    (string * typ) list ->
    9.32 -    ((Name.binding * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory
    9.33 +    ((Name.binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
    9.34 +    thm list -> theory -> inductive_result * theory
    9.35    val arities_of: thm -> (string * int) list
    9.36    val params_of: thm -> term list
    9.37    val partition_rules: thm -> thm list -> (string * thm list) list
    9.38 @@ -70,14 +69,12 @@
    9.39      thm -> local_theory -> thm list * thm list * thm * local_theory
    9.40    val add_ind_def: add_ind_def
    9.41    val gen_add_inductive_i: add_ind_def -> inductive_flags ->
    9.42 -    ((Name.binding * typ) * mixfix) list ->
    9.43 -    (string * typ) list ->
    9.44 -    ((Name.binding * Attrib.src list) * term) list -> thm list ->
    9.45 -    local_theory -> inductive_result * local_theory
    9.46 +    ((Name.binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
    9.47 +    thm list -> local_theory -> inductive_result * local_theory
    9.48    val gen_add_inductive: add_ind_def -> bool -> bool ->
    9.49      (Name.binding * string option * mixfix) list ->
    9.50      (Name.binding * string option * mixfix) list ->
    9.51 -    ((Name.binding * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
    9.52 +    (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
    9.53      local_theory -> inductive_result * local_theory
    9.54    val gen_ind_decl: add_ind_def -> bool ->
    9.55      OuterParse.token list -> (local_theory -> local_theory) * OuterParse.token list
    9.56 @@ -648,7 +645,7 @@
    9.57      val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
    9.58        LocalTheory.define Thm.internalK
    9.59          ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
    9.60 -         ((Name.no_binding, []), fold_rev lambda params
    9.61 +         (Attrib.no_binding, fold_rev lambda params
    9.62             (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
    9.63      val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
    9.64        (cterm_of (ProofContext.theory_of ctxt') (list_comb (rec_const, params)));
    9.65 @@ -659,7 +656,7 @@
    9.66            val xs = map Free (Variable.variant_frees ctxt intr_ts
    9.67              (mk_names "x" (length Ts) ~~ Ts))
    9.68          in
    9.69 -          (name_mx, ((Name.no_binding, []), fold_rev lambda (params @ xs)
    9.70 +          (name_mx, (Attrib.no_binding, fold_rev lambda (params @ xs)
    9.71              (list_comb (rec_const, params @ make_bool_args' bs i @
    9.72                make_args argTs (xs ~~ Ts)))))
    9.73          end) (cnames_syn ~~ cs);
    9.74 @@ -726,7 +723,7 @@
    9.75  
    9.76  type add_ind_def =
    9.77    inductive_flags ->
    9.78 -  term list -> ((Name.binding * Attrib.src list) * term) list -> thm list ->
    9.79 +  term list -> (Attrib.binding * term) list -> thm list ->
    9.80    term list -> (Name.binding * mixfix) list ->
    9.81    local_theory -> inductive_result * local_theory
    9.82  
    10.1 --- a/src/HOL/Tools/inductive_set_package.ML	Tue Sep 02 14:10:45 2008 +0200
    10.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Tue Sep 02 16:55:33 2008 +0200
    10.3 @@ -14,11 +14,13 @@
    10.4    val add_inductive_i:
    10.5      InductivePackage.inductive_flags ->
    10.6      ((Name.binding * typ) * mixfix) list ->
    10.7 -    (string * typ) list -> ((Name.binding * Attrib.src list) * term) list -> thm list ->
    10.8 -      local_theory -> InductivePackage.inductive_result * local_theory
    10.9 -  val add_inductive: bool -> bool -> (Name.binding * string option * mixfix) list ->
   10.10 +    (string * typ) list ->
   10.11 +    (Attrib.binding * term) list -> thm list ->
   10.12 +    local_theory -> InductivePackage.inductive_result * local_theory
   10.13 +  val add_inductive: bool -> bool ->
   10.14      (Name.binding * string option * mixfix) list ->
   10.15 -    ((Name.binding * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
   10.16 +    (Name.binding * string option * mixfix) list ->
   10.17 +    (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
   10.18      local_theory -> InductivePackage.inductive_result * local_theory
   10.19    val setup: theory -> theory
   10.20  end;
   10.21 @@ -471,7 +473,7 @@
   10.22  
   10.23      (* define inductive sets using previously defined predicates *)
   10.24      val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
   10.25 -      (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, ((Name.no_binding, []),
   10.26 +      (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.no_binding,
   10.27           fold_rev lambda params (HOLogic.Collect_const U $
   10.28             HOLogic.ap_split' fs U HOLogic.boolT (list_comb (p, params3))))))
   10.29           (cnames_syn ~~ cs_info ~~ preds)) ctxt1;
    11.1 --- a/src/HOL/Tools/primrec_package.ML	Tue Sep 02 14:10:45 2008 +0200
    11.2 +++ b/src/HOL/Tools/primrec_package.ML	Tue Sep 02 16:55:33 2008 +0200
    11.3 @@ -9,12 +9,12 @@
    11.4  signature PRIMREC_PACKAGE =
    11.5  sig
    11.6    val add_primrec: (Name.binding * typ option * mixfix) list ->
    11.7 -    ((Name.binding * Attrib.src list) * term) list -> local_theory -> thm list * local_theory
    11.8 +    (Attrib.binding * term) list -> local_theory -> thm list * local_theory
    11.9    val add_primrec_global: (Name.binding * typ option * mixfix) list ->
   11.10 -    ((Name.binding * Attrib.src list) * term) list -> theory -> thm list * theory
   11.11 +    (Attrib.binding * term) list -> theory -> thm list * theory
   11.12    val add_primrec_overloaded: (string * (string * typ) * bool) list ->
   11.13      (Name.binding * typ option * mixfix) list ->
   11.14 -    ((Name.binding * Attrib.src list) * term) list -> theory -> thm list * theory
   11.15 +    (Attrib.binding * term) list -> theory -> thm list * theory
   11.16  end;
   11.17  
   11.18  structure PrimrecPackage : PRIMREC_PACKAGE =
    12.1 --- a/src/HOL/Tools/recdef_package.ML	Tue Sep 02 14:10:45 2008 +0200
    12.2 +++ b/src/HOL/Tools/recdef_package.ML	Tue Sep 02 16:55:33 2008 +0200
    12.3 @@ -269,7 +269,7 @@
    12.4          " in recdef definition of " ^ quote name);
    12.5    in
    12.6      Specification.theorem Thm.internalK NONE (K I) (Name.binding bname, atts)
    12.7 -      [] (Element.Shows [((Name.no_binding, []), [(HOLogic.mk_Trueprop tc, [])])]) int lthy
    12.8 +      [] (Element.Shows [(Attrib.no_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
    12.9    end;
   12.10  
   12.11  val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const;
    13.1 --- a/src/HOL/Tools/typecopy_package.ML	Tue Sep 02 14:10:45 2008 +0200
    13.2 +++ b/src/HOL/Tools/typecopy_package.ML	Tue Sep 02 16:55:33 2008 +0200
    13.3 @@ -134,7 +134,7 @@
    13.4            (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
    13.5          val def' = Syntax.check_term lthy def;
    13.6          val ((_, (_, thm)), lthy') = Specification.definition
    13.7 -          (NONE, ((Name.no_binding, []), def')) lthy;
    13.8 +          (NONE, (Attrib.no_binding, def')) lthy;
    13.9          val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
   13.10          val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
   13.11        in (thm', lthy') end;
    14.1 --- a/src/HOL/Typedef.thy	Tue Sep 02 14:10:45 2008 +0200
    14.2 +++ b/src/HOL/Typedef.thy	Tue Sep 02 16:55:33 2008 +0200
    14.3 @@ -145,7 +145,7 @@
    14.4      thy
    14.5      |> TheoryTarget.instantiation ([tyco], vs, @{sort itself})
    14.6      |> `(fn lthy => Syntax.check_term lthy eq)
    14.7 -    |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
    14.8 +    |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
    14.9      |> snd
   14.10      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   14.11      |> LocalTheory.exit
    15.1 --- a/src/HOL/ex/Quickcheck.thy	Tue Sep 02 14:10:45 2008 +0200
    15.2 +++ b/src/HOL/ex/Quickcheck.thy	Tue Sep 02 16:55:33 2008 +0200
    15.3 @@ -132,7 +132,7 @@
    15.4                   (map (fn eq => ((Name.no_binding, [del_func]), eq)) eqs')
    15.5            |-> add_code
    15.6            |> `(fn lthy => Syntax.check_term lthy eq)
    15.7 -          |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
    15.8 +          |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
    15.9            |> snd
   15.10            |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   15.11            |> LocalTheory.exit
   15.12 @@ -261,7 +261,7 @@
   15.13    in
   15.14      thy
   15.15      |> TheoryTarget.init NONE
   15.16 -    |> Specification.definition (NONE, ((Name.no_binding, []), eq))
   15.17 +    |> Specification.definition (NONE, (Attrib.no_binding, eq))
   15.18      |> snd
   15.19      |> LocalTheory.exit
   15.20      |> ProofContext.theory_of
    16.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Tue Sep 02 14:10:45 2008 +0200
    16.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Tue Sep 02 16:55:33 2008 +0200
    16.3 @@ -9,9 +9,9 @@
    16.4  sig
    16.5    val legacy_infer_term: theory -> term -> term
    16.6    val legacy_infer_prop: theory -> term -> term
    16.7 -  val add_fixrec: bool -> ((Name.binding * Attrib.src list) * string) list list -> theory -> theory
    16.8 +  val add_fixrec: bool -> (Attrib.binding * string) list list -> theory -> theory
    16.9    val add_fixrec_i: bool -> ((Name.binding * attribute list) * term) list list -> theory -> theory
   16.10 -  val add_fixpat: (Name.binding * Attrib.src list) * string list -> theory -> theory
   16.11 +  val add_fixpat: Attrib.binding * string list -> theory -> theory
   16.12    val add_fixpat_i: (Name.binding * attribute list) * term list -> theory -> theory
   16.13  end;
   16.14  
    17.1 --- a/src/Pure/Isar/attrib.ML	Tue Sep 02 14:10:45 2008 +0200
    17.2 +++ b/src/Pure/Isar/attrib.ML	Tue Sep 02 16:55:33 2008 +0200
    17.3 @@ -8,6 +8,8 @@
    17.4  signature ATTRIB =
    17.5  sig
    17.6    type src = Args.src
    17.7 +  type binding = Name.binding * src list
    17.8 +  val no_binding: binding
    17.9    val print_attributes: theory -> unit
   17.10    val intern: theory -> xstring -> string
   17.11    val intern_src: theory -> src -> src
   17.12 @@ -48,8 +50,15 @@
   17.13  structure T = OuterLex;
   17.14  structure P = OuterParse;
   17.15  
   17.16 +
   17.17 +(* source and bindings *)
   17.18 +
   17.19  type src = Args.src;
   17.20  
   17.21 +type binding = Name.binding * src list;
   17.22 +val no_binding: binding = (Name.no_binding, []);
   17.23 +
   17.24 +
   17.25  
   17.26  (** named attributes **)
   17.27  
    18.1 --- a/src/Pure/Isar/class.ML	Tue Sep 02 14:10:45 2008 +0200
    18.2 +++ b/src/Pure/Isar/class.ML	Tue Sep 02 16:55:33 2008 +0200
    18.3 @@ -19,7 +19,7 @@
    18.4    val abbrev: class -> Syntax.mode -> Properties.T
    18.5      -> (string * mixfix) * term -> theory -> theory
    18.6    val note: class -> string
    18.7 -    -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list
    18.8 +    -> (Attrib.binding * (thm list * Attrib.src list) list) list
    18.9      -> theory -> (bstring * thm list) list * theory
   18.10    val declaration: class -> declaration -> theory -> theory
   18.11    val refresh_syntax: class -> Proof.context -> Proof.context
   18.12 @@ -48,7 +48,7 @@
   18.13  
   18.14    (*old axclass layer*)
   18.15    val axclass_cmd: bstring * xstring list
   18.16 -    -> ((Name.binding * Attrib.src list) * string list) list
   18.17 +    -> (Attrib.binding * string list) list
   18.18      -> theory -> class * theory
   18.19    val classrel_cmd: xstring * xstring -> theory -> Proof.state
   18.20  
   18.21 @@ -374,7 +374,7 @@
   18.22      thy
   18.23      |> fold2 add_constraint (map snd consts) no_constraints
   18.24      |> prove_interpretation tac ((false, prfx), []) (Locale.Locale class)
   18.25 -          (inst, map (fn def => ((Name.no_binding, []), def)) defs)
   18.26 +          (inst, map (fn def => (Attrib.no_binding, def)) defs)
   18.27      |> fold2 add_constraint (map snd consts) constraints
   18.28    end;
   18.29  
    19.1 --- a/src/Pure/Isar/constdefs.ML	Tue Sep 02 14:10:45 2008 +0200
    19.2 +++ b/src/Pure/Isar/constdefs.ML	Tue Sep 02 16:55:33 2008 +0200
    19.3 @@ -11,7 +11,7 @@
    19.4  sig
    19.5    val add_constdefs: (Name.binding * string option) list *
    19.6      ((Name.binding * string option * mixfix) option *
    19.7 -      ((Name.binding * Attrib.src list) * string)) list -> theory -> theory
    19.8 +      (Attrib.binding * string)) list -> theory -> theory
    19.9    val add_constdefs_i: (Name.binding * typ option) list *
   19.10      ((Name.binding * typ option * mixfix) option *
   19.11        ((Name.binding * attribute list) * term)) list -> theory -> theory
    20.1 --- a/src/Pure/Isar/element.ML	Tue Sep 02 14:10:45 2008 +0200
    20.2 +++ b/src/Pure/Isar/element.ML	Tue Sep 02 16:55:33 2008 +0200
    20.3 @@ -9,21 +9,21 @@
    20.4  signature ELEMENT =
    20.5  sig
    20.6    datatype ('typ, 'term) stmt =
    20.7 -    Shows of ((Name.binding * Attrib.src list) * ('term * 'term list) list) list |
    20.8 +    Shows of (Attrib.binding * ('term * 'term list) list) list |
    20.9      Obtains of (Name.binding * ((Name.binding * 'typ option) list * 'term list)) list
   20.10    type statement = (string, string) stmt
   20.11    type statement_i = (typ, term) stmt
   20.12    datatype ('typ, 'term, 'fact) ctxt =
   20.13      Fixes of (Name.binding * 'typ option * mixfix) list |
   20.14      Constrains of (string * 'typ) list |
   20.15 -    Assumes of ((Name.binding * Attrib.src list) * ('term * 'term list) list) list |
   20.16 -    Defines of ((Name.binding * Attrib.src list) * ('term * 'term list)) list |
   20.17 -    Notes of string * ((Name.binding * Attrib.src list) * ('fact * Attrib.src list) list) list
   20.18 +    Assumes of (Attrib.binding * ('term * 'term list) list) list |
   20.19 +    Defines of (Attrib.binding * ('term * 'term list)) list |
   20.20 +    Notes of string * (Attrib.binding * ('fact * Attrib.src list) list) list
   20.21    type context = (string, string, Facts.ref) ctxt
   20.22    type context_i = (typ, term, thm list) ctxt
   20.23    val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) ->
   20.24 -   ((Name.binding * Attrib.src list) * ('fact * Attrib.src list) list) list ->
   20.25 -   ((Name.binding * Attrib.src list) * ('c * Attrib.src list) list) list
   20.26 +   (Attrib.binding * ('fact * Attrib.src list) list) list ->
   20.27 +   (Attrib.binding * ('c * Attrib.src list) list) list
   20.28    val map_ctxt: {name: Name.binding -> Name.binding,
   20.29      var: Name.binding * mixfix -> Name.binding * mixfix,
   20.30      typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
   20.31 @@ -33,8 +33,7 @@
   20.32    val morph_ctxt: morphism -> context_i -> context_i
   20.33    val params_of: context_i -> (string * typ) list
   20.34    val prems_of: context_i -> term list
   20.35 -  val facts_of: theory -> context_i ->
   20.36 -    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list
   20.37 +  val facts_of: theory -> context_i -> (Attrib.binding * (thm list * Attrib.src list) list) list
   20.38    val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
   20.39    val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
   20.40    val pretty_statement: Proof.context -> string -> thm -> Pretty.T
   20.41 @@ -71,11 +70,11 @@
   20.42    val satisfy_thm: witness list -> thm -> thm
   20.43    val satisfy_morphism: witness list -> morphism
   20.44    val satisfy_facts: witness list ->
   20.45 -    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
   20.46 -    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list
   20.47 +    (Attrib.binding * (thm list * Attrib.src list) list) list ->
   20.48 +    (Attrib.binding * (thm list * Attrib.src list) list) list
   20.49    val generalize_facts: Proof.context -> Proof.context ->
   20.50 -    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
   20.51 -    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list
   20.52 +    (Attrib.binding * (thm list * Attrib.src list) list) list ->
   20.53 +    (Attrib.binding * (thm list * Attrib.src list) list) list
   20.54  end;
   20.55  
   20.56  structure Element: ELEMENT =
   20.57 @@ -86,7 +85,7 @@
   20.58  (* statement *)
   20.59  
   20.60  datatype ('typ, 'term) stmt =
   20.61 -  Shows of ((Name.binding * Attrib.src list) * ('term * 'term list) list) list |
   20.62 +  Shows of (Attrib.binding * ('term * 'term list) list) list |
   20.63    Obtains of (Name.binding * ((Name.binding * 'typ option) list * 'term list)) list;
   20.64  
   20.65  type statement = (string, string) stmt;
   20.66 @@ -98,9 +97,9 @@
   20.67  datatype ('typ, 'term, 'fact) ctxt =
   20.68    Fixes of (Name.binding * 'typ option * mixfix) list |
   20.69    Constrains of (string * 'typ) list |
   20.70 -  Assumes of ((Name.binding * Attrib.src list) * ('term * 'term list) list) list |
   20.71 -  Defines of ((Name.binding * Attrib.src list) * ('term * 'term list)) list |
   20.72 -  Notes of string * ((Name.binding * Attrib.src list) * ('fact * Attrib.src list) list) list;
   20.73 +  Assumes of (Attrib.binding * ('term * 'term list) list) list |
   20.74 +  Defines of (Attrib.binding * ('term * 'term list)) list |
   20.75 +  Notes of string * (Attrib.binding * ('fact * Attrib.src list) list) list;
   20.76  
   20.77  type context = (string, string, Facts.ref) ctxt;
   20.78  type context_i = (typ, term, thm list) ctxt;
   20.79 @@ -272,8 +271,8 @@
   20.80        is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
   20.81    in
   20.82      pretty_ctxt ctxt' (Fixes (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) fixes)) @
   20.83 -    pretty_ctxt ctxt' (Assumes (map (fn t => ((Name.no_binding, []), [(t, [])])) assumes)) @
   20.84 -     (if null cases then pretty_stmt ctxt' (Shows [((Name.no_binding, []), [(concl, [])])])
   20.85 +    pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.no_binding, [(t, [])])) assumes)) @
   20.86 +     (if null cases then pretty_stmt ctxt' (Shows [(Attrib.no_binding, [(concl, [])])])
   20.87        else
   20.88          let val (clauses, ctxt'') = fold_map (obtain o cert) cases ctxt'
   20.89          in pretty_stmt ctxt'' (Obtains clauses) end)
    21.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Sep 02 14:10:45 2008 +0200
    21.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Sep 02 16:55:33 2008 +0200
    21.3 @@ -21,14 +21,10 @@
    21.4    val simproc_setup: string -> string list -> string * Position.T -> string list ->
    21.5      local_theory -> local_theory
    21.6    val hide_names: bool -> string * xstring list -> theory -> theory
    21.7 -  val have: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
    21.8 -    bool -> Proof.state -> Proof.state
    21.9 -  val hence: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
   21.10 -    bool -> Proof.state -> Proof.state
   21.11 -  val show: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
   21.12 -    bool -> Proof.state -> Proof.state
   21.13 -  val thus: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
   21.14 -    bool -> Proof.state -> Proof.state
   21.15 +  val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   21.16 +  val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   21.17 +  val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   21.18 +  val thus: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   21.19    val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
   21.20    val terminal_proof: Method.text * Method.text option ->
   21.21      Toplevel.transition -> Toplevel.transition
    22.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Sep 02 14:10:45 2008 +0200
    22.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 02 16:55:33 2008 +0200
    22.3 @@ -272,7 +272,7 @@
    22.4  val _ =
    22.5    OuterSyntax.local_theory "declare" "declare theorems (improper)" K.thy_decl
    22.6      (P.and_list1 SpecParse.xthms1
    22.7 -      >> (fn args => #2 o Specification.theorems_cmd "" [((Name.no_binding, []), flat args)]));
    22.8 +      >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.no_binding, flat args)]));
    22.9  
   22.10  
   22.11  (* name space entry path *)
   22.12 @@ -468,7 +468,7 @@
   22.13  fun gen_theorem kind =
   22.14    OuterSyntax.local_theory_to_proof' kind ("state " ^ kind) K.thy_goal
   22.15      (Scan.optional (SpecParse.opt_thm_name ":" --|
   22.16 -      Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) (Name.no_binding, []) --
   22.17 +      Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) Attrib.no_binding --
   22.18        SpecParse.general_statement >> (fn (a, (elems, concl)) =>
   22.19          (Specification.theorem_cmd kind NONE (K I) a elems concl)));
   22.20  
    23.1 --- a/src/Pure/Isar/local_theory.ML	Tue Sep 02 14:10:45 2008 +0200
    23.2 +++ b/src/Pure/Isar/local_theory.ML	Tue Sep 02 16:55:33 2008 +0200
    23.3 @@ -26,15 +26,14 @@
    23.4    val affirm: local_theory -> local_theory
    23.5    val pretty: local_theory -> Pretty.T list
    23.6    val axioms: string ->
    23.7 -    ((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list -> local_theory
    23.8 +    ((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list -> local_theory
    23.9      -> (term list * (string * thm list) list) * local_theory
   23.10    val abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
   23.11      (term * term) * local_theory
   23.12 -  val define: string -> (Name.binding * mixfix) * ((Name.binding * Attrib.src list) * term) -> local_theory ->
   23.13 +  val define: string -> (Name.binding * mixfix) * (Attrib.binding * term) -> local_theory ->
   23.14      (term * (string * thm)) * local_theory
   23.15 -  val note: string -> (Name.binding * Attrib.src list) * thm list ->
   23.16 -    local_theory -> (string * thm list) * local_theory
   23.17 -  val notes: string -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
   23.18 +  val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
   23.19 +  val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
   23.20      local_theory -> (string * thm list) list * local_theory
   23.21    val type_syntax: declaration -> local_theory -> local_theory
   23.22    val term_syntax: declaration -> local_theory -> local_theory
   23.23 @@ -57,14 +56,15 @@
   23.24  type operations =
   23.25   {pretty: local_theory -> Pretty.T list,
   23.26    axioms: string ->
   23.27 -    ((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list -> local_theory
   23.28 -    -> (term list * (string * thm list) list) * local_theory,
   23.29 -  abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory -> (term * term) * local_theory,
   23.30 +    ((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list -> local_theory ->
   23.31 +    (term list * (string * thm list) list) * local_theory,
   23.32 +  abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
   23.33 +    (term * term) * local_theory,
   23.34    define: string ->
   23.35 -    (Name.binding * mixfix) * ((Name.binding * Attrib.src list) * term) -> local_theory ->
   23.36 +    (Name.binding * mixfix) * (Attrib.binding * term) -> local_theory ->
   23.37      (term * (string * thm)) * local_theory,
   23.38    notes: string ->
   23.39 -    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
   23.40 +    (Attrib.binding * (thm list * Attrib.src list) list) list ->
   23.41      local_theory -> (string * thm list) list * local_theory,
   23.42    type_syntax: declaration -> local_theory -> local_theory,
   23.43    term_syntax: declaration -> local_theory -> local_theory,
    24.1 --- a/src/Pure/Isar/locale.ML	Tue Sep 02 14:10:45 2008 +0200
    24.2 +++ b/src/Pure/Isar/locale.ML	Tue Sep 02 16:55:33 2008 +0200
    24.3 @@ -50,21 +50,16 @@
    24.4    val init: string -> theory -> Proof.context
    24.5  
    24.6    (* The specification of a locale *)
    24.7 -  val parameters_of: theory -> string ->
    24.8 -    ((string * typ) * mixfix) list
    24.9 -  val parameters_of_expr: theory -> expr ->
   24.10 -    ((string * typ) * mixfix) list
   24.11 -  val local_asms_of: theory -> string ->
   24.12 -    ((Name.binding * Attrib.src list) * term list) list
   24.13 -  val global_asms_of: theory -> string ->
   24.14 -    ((Name.binding * Attrib.src list) * term list) list
   24.15 +  val parameters_of: theory -> string -> ((string * typ) * mixfix) list
   24.16 +  val parameters_of_expr: theory -> expr -> ((string * typ) * mixfix) list
   24.17 +  val local_asms_of: theory -> string -> (Attrib.binding * term list) list
   24.18 +  val global_asms_of: theory -> string -> (Attrib.binding * term list) list
   24.19  
   24.20    (* Theorems *)
   24.21    val intros: theory -> string -> thm list * thm list
   24.22    val dests: theory -> string -> thm list
   24.23    (* Not part of the official interface.  DO NOT USE *)
   24.24 -  val facts_of: theory -> string
   24.25 -    -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list list
   24.26 +  val facts_of: theory -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list list
   24.27  
   24.28    (* Processing of locale statements *)
   24.29    val read_context_statement: xstring option -> Element.context element list ->
   24.30 @@ -95,8 +90,7 @@
   24.31    val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
   24.32  
   24.33    (* Storing results *)
   24.34 -  val add_thmss: string -> string ->
   24.35 -    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
   24.36 +  val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
   24.37      Proof.context -> Proof.context
   24.38    val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
   24.39    val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
   24.40 @@ -104,21 +98,21 @@
   24.41  
   24.42    val interpretation_i: (Proof.context -> Proof.context) ->
   24.43      (bool * string) * Attrib.src list -> expr ->
   24.44 -    term option list * ((Name.binding * Attrib.src list) * term) list ->
   24.45 +    term option list * (Attrib.binding * term) list ->
   24.46      theory -> Proof.state
   24.47    val interpretation: (Proof.context -> Proof.context) ->
   24.48      (bool * string) * Attrib.src list -> expr ->
   24.49 -    string option list * ((Name.binding * Attrib.src list) * string) list ->
   24.50 +    string option list * (Attrib.binding * string) list ->
   24.51      theory -> Proof.state
   24.52    val interpretation_in_locale: (Proof.context -> Proof.context) ->
   24.53      xstring * expr -> theory -> Proof.state
   24.54    val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
   24.55      (bool * string) * Attrib.src list -> expr ->
   24.56 -    term option list * ((Name.binding * Attrib.src list) * term) list ->
   24.57 +    term option list * (Attrib.binding * term) list ->
   24.58      bool -> Proof.state -> Proof.state
   24.59    val interpret: (Proof.state -> Proof.state Seq.seq) ->
   24.60      (bool * string) * Attrib.src list -> expr ->
   24.61 -    string option list * ((Name.binding * Attrib.src list) * string) list ->
   24.62 +    string option list * (Attrib.binding * string) list ->
   24.63      bool -> Proof.state -> Proof.state
   24.64  end;
   24.65  
   24.66 @@ -1275,8 +1269,7 @@
   24.67      list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
   24.68        Term.fast_term_ord (d1, d2)) (defs1, defs2);
   24.69  structure Defstab =
   24.70 -    TableFun(type key = ((Name.binding * Attrib.src list) * (term * term list)) list
   24.71 -        val ord = defs_ord);
   24.72 +    TableFun(type key = (Attrib.binding * (term * term list)) list val ord = defs_ord);
   24.73  
   24.74  fun rem_dup_defs es ds =
   24.75      fold_map (fn e as (Defines defs) => (fn ds =>
   24.76 @@ -1908,7 +1901,7 @@
   24.77  
   24.78  fun defines_to_notes is_ext thy (Defines defs) defns =
   24.79      let
   24.80 -      val defs' = map (fn (_, (def, _)) => ((Name.no_binding, []), (def, []))) defs
   24.81 +      val defs' = map (fn (_, (def, _)) => (Attrib.no_binding, (def, []))) defs
   24.82        val notes = map (fn (a, (def, _)) =>
   24.83          (a, [([assume (cterm_of thy def)], [])])) defs
   24.84      in
    25.1 --- a/src/Pure/Isar/obtain.ML	Tue Sep 02 14:10:45 2008 +0200
    25.2 +++ b/src/Pure/Isar/obtain.ML	Tue Sep 02 16:55:33 2008 +0200
    25.3 @@ -41,7 +41,7 @@
    25.4  sig
    25.5    val thatN: string
    25.6    val obtain: string -> (Name.binding * string option * mixfix) list ->
    25.7 -    ((Name.binding * Attrib.src list) * (string * string list) list) list ->
    25.8 +    (Attrib.binding * (string * string list) list) list ->
    25.9      bool -> Proof.state -> Proof.state
   25.10    val obtain_i: string -> (Name.binding * typ option * mixfix) list ->
   25.11      ((Name.binding * attribute list) * (term * term list) list) list ->
    26.1 --- a/src/Pure/Isar/proof.ML	Tue Sep 02 14:10:45 2008 +0200
    26.2 +++ b/src/Pure/Isar/proof.ML	Tue Sep 02 16:55:33 2008 +0200
    26.3 @@ -47,26 +47,23 @@
    26.4    val fix: (Name.binding * string option * mixfix) list -> state -> state
    26.5    val fix_i: (Name.binding * typ option * mixfix) list -> state -> state
    26.6    val assm: Assumption.export ->
    26.7 -    ((Name.binding * Attrib.src list) * (string * string list) list) list -> state -> state
    26.8 +    (Attrib.binding * (string * string list) list) list -> state -> state
    26.9    val assm_i: Assumption.export ->
   26.10      ((Name.binding * attribute list) * (term * term list) list) list -> state -> state
   26.11 -  val assume: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
   26.12 -    state -> state
   26.13 +  val assume: (Attrib.binding * (string * string list) list) list -> state -> state
   26.14    val assume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
   26.15      state -> state
   26.16 -  val presume: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
   26.17 -    state -> state
   26.18 +  val presume: (Attrib.binding * (string * string list) list) list -> state -> state
   26.19    val presume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
   26.20      state -> state
   26.21 -  val def: ((Name.binding * Attrib.src list) *
   26.22 -    ((Name.binding * mixfix) * (string * string list))) list -> state -> state
   26.23 +  val def: (Attrib.binding * ((Name.binding * mixfix) * (string * string list))) list ->
   26.24 +    state -> state
   26.25    val def_i: ((Name.binding * attribute list) *
   26.26      ((Name.binding * mixfix) * (term * term list))) list -> state -> state
   26.27    val chain: state -> state
   26.28    val chain_facts: thm list -> state -> state
   26.29    val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
   26.30 -  val note_thmss: ((Name.binding * Attrib.src list) *
   26.31 -    (Facts.ref * Attrib.src list) list) list -> state -> state
   26.32 +  val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
   26.33    val note_thmss_i: ((Name.binding * attribute list) *
   26.34      (thm list * attribute list) list) list -> state -> state
   26.35    val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
   26.36 @@ -109,11 +106,11 @@
   26.37    val global_done_proof: state -> context
   26.38    val global_skip_proof: bool -> state -> context
   26.39    val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   26.40 -    ((Name.binding * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
   26.41 +    (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   26.42    val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   26.43      ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
   26.44    val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   26.45 -    ((Name.binding * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
   26.46 +    (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   26.47    val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   26.48      ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
   26.49  end;
    27.1 --- a/src/Pure/Isar/spec_parse.ML	Tue Sep 02 14:10:45 2008 +0200
    27.2 +++ b/src/Pure/Isar/spec_parse.ML	Tue Sep 02 16:55:33 2008 +0200
    27.3 @@ -11,34 +11,31 @@
    27.4    val attrib: OuterLex.token list -> Attrib.src * token list
    27.5    val attribs: token list -> Attrib.src list * token list
    27.6    val opt_attribs: token list -> Attrib.src list * token list
    27.7 -  val thm_name: string -> token list -> (Name.binding * Attrib.src list) * token list
    27.8 -  val opt_thm_name: string -> token list -> (Name.binding * Attrib.src list) * token list
    27.9 -  val spec: token list -> ((Name.binding * Attrib.src list) * string list) * token list
   27.10 -  val named_spec: token list -> ((Name.binding * Attrib.src list) * string list) * token list
   27.11 +  val thm_name: string -> token list -> Attrib.binding * token list
   27.12 +  val opt_thm_name: string -> token list -> Attrib.binding * token list
   27.13 +  val spec: token list -> (Attrib.binding * string list) * token list
   27.14 +  val named_spec: token list -> (Attrib.binding * string list) * token list
   27.15    val spec_name: token list -> ((Name.binding * string) * Attrib.src list) * token list
   27.16    val spec_opt_name: token list -> ((Name.binding * string) * Attrib.src list) * token list
   27.17    val xthm: token list -> (Facts.ref * Attrib.src list) * token list
   27.18    val xthms1: token list -> (Facts.ref * Attrib.src list) list * token list
   27.19    val name_facts: token list ->
   27.20 -    ((Name.binding * Attrib.src list) * (Facts.ref * Attrib.src list) list) list * token list
   27.21 +    (Attrib.binding * (Facts.ref * Attrib.src list) list) list * token list
   27.22    val locale_mixfix: token list -> mixfix * token list
   27.23    val locale_fixes: token list -> (Name.binding * string option * mixfix) list * token list
   27.24 -  val locale_insts: token list ->
   27.25 -    (string option list * ((Name.binding * Attrib.src list) * string) list) * token list
   27.26 +  val locale_insts: token list -> (string option list * (Attrib.binding * string) list) * token list
   27.27    val class_expr: token list -> string list * token list
   27.28    val locale_expr: token list -> Locale.expr * token list
   27.29    val locale_keyword: token list -> string * token list
   27.30    val locale_element: token list -> Element.context Locale.element * token list
   27.31    val context_element: token list -> Element.context * token list
   27.32 -  val statement: token list ->
   27.33 -    ((Name.binding * Attrib.src list) * (string * string list) list) list * token list
   27.34 +  val statement: token list -> (Attrib.binding * (string * string list) list) list * token list
   27.35    val general_statement: token list ->
   27.36      (Element.context Locale.element list * Element.statement) * OuterLex.token list
   27.37    val statement_keyword: token list -> string * token list
   27.38    val specification: token list ->
   27.39      (Name.binding *
   27.40 -      (((Name.binding * Attrib.src list) * string list) list *
   27.41 -        (Name.binding * string option) list)) list * token list
   27.42 +      ((Attrib.binding * string list) list * (Name.binding * string option) list)) list * token list
   27.43  end;
   27.44  
   27.45  structure SpecParse: SPEC_PARSE =
   27.46 @@ -58,7 +55,7 @@
   27.47  
   27.48  fun opt_thm_name s =
   27.49    Scan.optional ((P.binding -- opt_attribs || attribs >> pair Name.no_binding) --| P.$$$ s)
   27.50 -    (Name.no_binding, []);
   27.51 +    Attrib.no_binding;
   27.52  
   27.53  val spec = opt_thm_name ":" -- Scan.repeat1 P.prop;
   27.54  val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
    28.1 --- a/src/Pure/Isar/specification.ML	Tue Sep 02 14:10:45 2008 +0200
    28.2 +++ b/src/Pure/Isar/specification.ML	Tue Sep 02 16:55:33 2008 +0200
    28.3 @@ -10,32 +10,28 @@
    28.4  sig
    28.5    val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
    28.6    val check_specification: (Name.binding * typ option * mixfix) list ->
    28.7 -    ((Name.binding * Attrib.src list) * term list) list list -> Proof.context ->
    28.8 -    (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
    28.9 -    Proof.context
   28.10 +    (Attrib.binding * term list) list list -> Proof.context ->
   28.11 +    (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   28.12    val read_specification: (Name.binding * string option * mixfix) list ->
   28.13 -    ((Name.binding * Attrib.src list) * string list) list list -> Proof.context ->
   28.14 -    (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
   28.15 -    Proof.context
   28.16 +    (Attrib.binding * string list) list list -> Proof.context ->
   28.17 +    (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   28.18    val check_free_specification: (Name.binding * typ option * mixfix) list ->
   28.19 -    ((Name.binding * Attrib.src list) * term list) list -> Proof.context ->
   28.20 -    (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
   28.21 -    Proof.context
   28.22 +    (Attrib.binding * term list) list -> Proof.context ->
   28.23 +    (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   28.24    val read_free_specification: (Name.binding * string option * mixfix) list ->
   28.25 -    ((Name.binding * Attrib.src list) * string list) list -> Proof.context ->
   28.26 -    (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
   28.27 -    Proof.context
   28.28 +    (Attrib.binding * string list) list -> Proof.context ->
   28.29 +    (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   28.30    val axiomatization: (Name.binding * typ option * mixfix) list ->
   28.31 -    ((Name.binding * Attrib.src list) * term list) list -> local_theory ->
   28.32 +    (Attrib.binding * term list) list -> local_theory ->
   28.33      (term list * (string * thm list) list) * local_theory
   28.34    val axiomatization_cmd: (Name.binding * string option * mixfix) list ->
   28.35 -    ((Name.binding * Attrib.src list) * string list) list -> local_theory ->
   28.36 +    (Attrib.binding * string list) list -> local_theory ->
   28.37      (term list * (string * thm list) list) * local_theory
   28.38    val definition:
   28.39 -    (Name.binding * typ option * mixfix) option * ((Name.binding * Attrib.src list) * term) ->
   28.40 +    (Name.binding * typ option * mixfix) option * (Attrib.binding * term) ->
   28.41      local_theory -> (term * (string * thm)) * local_theory
   28.42    val definition_cmd:
   28.43 -    (Name.binding * string option * mixfix) option * ((Name.binding * Attrib.src list) * string) ->
   28.44 +    (Name.binding * string option * mixfix) option * (Attrib.binding * string) ->
   28.45      local_theory -> (term * (string * thm)) * local_theory
   28.46    val abbreviation: Syntax.mode -> (Name.binding * typ option * mixfix) option * term ->
   28.47      local_theory -> local_theory
   28.48 @@ -44,17 +40,17 @@
   28.49    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   28.50    val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   28.51    val theorems: string ->
   28.52 -    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
   28.53 +    (Attrib.binding * (thm list * Attrib.src list) list) list ->
   28.54      local_theory -> (string * thm list) list * local_theory
   28.55    val theorems_cmd: string ->
   28.56 -    ((Name.binding * Attrib.src list) * (Facts.ref * Attrib.src list) list) list ->
   28.57 +    (Attrib.binding * (Facts.ref * Attrib.src list) list) list ->
   28.58      local_theory -> (string * thm list) list * local_theory
   28.59    val theorem: string -> Method.text option ->
   28.60 -    (thm list list -> local_theory -> local_theory) -> Name.binding * Attrib.src list ->
   28.61 +    (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
   28.62      Element.context_i Locale.element list -> Element.statement_i ->
   28.63      bool -> local_theory -> Proof.state
   28.64    val theorem_cmd: string -> Method.text option ->
   28.65 -    (thm list list -> local_theory -> local_theory) -> Name.binding * Attrib.src list ->
   28.66 +    (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
   28.67      Element.context Locale.element list -> Element.statement ->
   28.68      bool -> local_theory -> Proof.state
   28.69    val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
    29.1 --- a/src/Pure/Isar/theory_target.ML	Tue Sep 02 14:10:45 2008 +0200
    29.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Sep 02 16:55:33 2008 +0200
    29.3 @@ -51,7 +51,7 @@
    29.4      val fixes = map (fn (x, T) =>
    29.5        (Name.binding x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
    29.6      val assumes = map (fn A =>
    29.7 -      ((Name.no_binding, []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
    29.8 +      (Attrib.no_binding, [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
    29.9      val elems =
   29.10        (if null fixes then [] else [Element.Fixes fixes]) @
   29.11        (if null assumes then [] else [Element.Assumes assumes]);
    30.1 --- a/src/ZF/Tools/ind_cases.ML	Tue Sep 02 14:10:45 2008 +0200
    30.2 +++ b/src/ZF/Tools/ind_cases.ML	Tue Sep 02 16:55:33 2008 +0200
    30.3 @@ -8,7 +8,7 @@
    30.4  signature IND_CASES =
    30.5  sig
    30.6    val declare: string -> (simpset -> cterm -> thm) -> theory -> theory
    30.7 -  val inductive_cases: ((Name.binding * Attrib.src list) * string list) list -> theory -> theory
    30.8 +  val inductive_cases: (Attrib.binding * string list) list -> theory -> theory
    30.9    val setup: theory -> theory
   30.10  end;
   30.11