# HG changeset patch
# User wenzelm
# Date 1220367333 -7200
# Node ID a05ca48ef263bdc990b38f88428bb0402d4018b2
# Parent  103d9282a946a5b4e85b8b28e3547c3040e9f382
type Attrib.binding abbreviates Name.binding without attributes;
Attrib.no_binding refers to Name.no_binding;

diff -r 103d9282a946 -r a05ca48ef263 src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOL/Library/Eval.thy	Tue Sep 02 16:55:33 2008 +0200
@@ -68,7 +68,7 @@
       thy
       |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
       |> `(fn lthy => Syntax.check_term lthy eq)
-      |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
+      |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
       |> snd
       |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
       |> LocalTheory.exit
diff -r 103d9282a946 -r a05ca48ef263 src/HOL/Library/RType.thy
--- a/src/HOL/Library/RType.thy	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOL/Library/RType.thy	Tue Sep 02 16:55:33 2008 +0200
@@ -67,7 +67,7 @@
     thy
     |> TheoryTarget.instantiation ([tyco], vs, @{sort rtype})
     |> `(fn lthy => Syntax.check_term lthy eq)
-    |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
+    |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
     |> snd
     |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
     |> LocalTheory.exit
diff -r 103d9282a946 -r a05ca48ef263 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -286,7 +286,7 @@
               else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
             end;
         in
-          ((Name.no_binding, []), HOLogic.mk_Trueprop (HOLogic.mk_eq
+          (Attrib.no_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
             (Free (nth perm_names_types' i) $
                Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
                list_comb (c, args),
@@ -563,7 +563,7 @@
            skip_mono = true}
           (map (fn (s, T) => ((Name.binding s, T --> HOLogic.boolT), NoSyn))
              (rep_set_names' ~~ recTs'))
-          [] (map (fn x => ((Name.no_binding, []), x)) intr_ts) [] thy3;
+          [] (map (fn x => (Attrib.no_binding, x)) intr_ts) [] thy3;
 
     (**** Prove that representing set is closed under permutation ****)
 
@@ -1480,7 +1480,7 @@
            skip_mono = true}
           (map (fn (s, T) => ((Name.binding s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
           (map dest_Free rec_fns)
-          (map (fn x => ((Name.no_binding, []), x)) rec_intr_ts) [] ||>
+          (map (fn x => (Attrib.no_binding, x)) rec_intr_ts) [] ||>
       PureThy.hide_fact true (NameSpace.append (Sign.full_name thy10 big_rec_name) "induct");
 
     (** equivariance **)
diff -r 103d9282a946 -r a05ca48ef263 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -160,7 +160,7 @@
             skip_mono = true}
           (map (fn (s, T) => ((Name.binding s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
           (map dest_Free rec_fns)
-          (map (fn x => ((Name.no_binding, []), x)) rec_intr_ts) [] thy0;
+          (map (fn x => (Attrib.no_binding, x)) rec_intr_ts) [] thy0;
 
     (* prove uniqueness and termination of primrec combinators *)
 
diff -r 103d9282a946 -r a05ca48ef263 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -442,7 +442,7 @@
           (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
         val def' = Syntax.check_term lthy def;
         val ((_, (_, thm)), lthy') = Specification.definition
-          (NONE, ((Name.no_binding, []), def')) lthy;
+          (NONE, (Attrib.no_binding, def')) lthy;
         val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
         val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
       in (thm', lthy') end;
diff -r 103d9282a946 -r a05ca48ef263 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -187,7 +187,7 @@
            alt_name = Name.binding big_rec_name, coind = false, no_elim = true, no_ind = false,
            skip_mono = true}
           (map (fn s => ((Name.binding s, UnivT'), NoSyn)) rep_set_names') []
-          (map (fn x => ((Name.no_binding, []), x)) intr_ts) [] thy1;
+          (map (fn x => (Attrib.no_binding, x)) intr_ts) [] thy1;
 
     (********************************* typedef ********************************)
 
diff -r 103d9282a946 -r a05ca48ef263 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -10,14 +10,14 @@
 signature FUNDEF_PACKAGE =
 sig
     val add_fundef :  (Name.binding * string option * mixfix) list
-                      -> ((Name.binding * Attrib.src list) * string) list 
+                      -> (Attrib.binding * string) list 
                       -> FundefCommon.fundef_config
                       -> bool list
                       -> local_theory
                       -> Proof.state
 
     val add_fundef_i:  (Name.binding * typ option * mixfix) list
-                       -> ((Name.binding * Attrib.src list) * term) list
+                       -> (Attrib.binding * term) list
                        -> FundefCommon.fundef_config
                        -> bool list
                        -> local_theory
diff -r 103d9282a946 -r a05ca48ef263 src/HOL/Tools/function_package/inductive_wrap.ML
--- a/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -51,7 +51,7 @@
               skip_mono = true}
             [((Name.binding R, T), NoSyn)] (* the relation *)
             [] (* no parameters *)
-            (map (fn t => ((Name.no_binding, []), t)) defs) (* the intros *)
+            (map (fn t => (Attrib.no_binding, t)) defs) (* the intros *)
             [] (* no special monos *)
             lthy
 
diff -r 103d9282a946 -r a05ca48ef263 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -33,25 +33,24 @@
   val inductive_forall_name: string
   val inductive_forall_def: thm
   val rulify: thm -> thm
-  val inductive_cases: ((Name.binding * Attrib.src list) * string list) list ->
-    Proof.context -> thm list list * local_theory
-  val inductive_cases_i: ((Name.binding * Attrib.src list) * term list) list ->
-    Proof.context -> thm list list * local_theory
+  val inductive_cases: (Attrib.binding * string list) list -> Proof.context ->
+    thm list list * local_theory
+  val inductive_cases_i: (Attrib.binding * term list) list -> Proof.context ->
+    thm list list * local_theory
   type inductive_flags
   val add_inductive_i:
     inductive_flags -> ((Name.binding * typ) * mixfix) list ->
-    (string * typ) list -> ((Name.binding * Attrib.src list) * term) list -> thm list ->
-      local_theory -> inductive_result * local_theory
+    (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
+    inductive_result * local_theory
   val add_inductive: bool -> bool ->
     (Name.binding * string option * mixfix) list ->
     (Name.binding * string option * mixfix) list ->
-    ((Name.binding * Attrib.src list) * string) list ->
+    (Attrib.binding * string) list ->
     (Facts.ref * Attrib.src list) list ->
     local_theory -> inductive_result * local_theory
   val add_inductive_global: string -> inductive_flags ->
-    ((Name.binding * typ) * mixfix) list ->
-    (string * typ) list ->
-    ((Name.binding * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory
+    ((Name.binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
+    thm list -> theory -> inductive_result * theory
   val arities_of: thm -> (string * int) list
   val params_of: thm -> term list
   val partition_rules: thm -> thm list -> (string * thm list) list
@@ -70,14 +69,12 @@
     thm -> local_theory -> thm list * thm list * thm * local_theory
   val add_ind_def: add_ind_def
   val gen_add_inductive_i: add_ind_def -> inductive_flags ->
-    ((Name.binding * typ) * mixfix) list ->
-    (string * typ) list ->
-    ((Name.binding * Attrib.src list) * term) list -> thm list ->
-    local_theory -> inductive_result * local_theory
+    ((Name.binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
+    thm list -> local_theory -> inductive_result * local_theory
   val gen_add_inductive: add_ind_def -> bool -> bool ->
     (Name.binding * string option * mixfix) list ->
     (Name.binding * string option * mixfix) list ->
-    ((Name.binding * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
+    (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
     local_theory -> inductive_result * local_theory
   val gen_ind_decl: add_ind_def -> bool ->
     OuterParse.token list -> (local_theory -> local_theory) * OuterParse.token list
@@ -648,7 +645,7 @@
     val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
       LocalTheory.define Thm.internalK
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
-         ((Name.no_binding, []), fold_rev lambda params
+         (Attrib.no_binding, fold_rev lambda params
            (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
     val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
       (cterm_of (ProofContext.theory_of ctxt') (list_comb (rec_const, params)));
@@ -659,7 +656,7 @@
           val xs = map Free (Variable.variant_frees ctxt intr_ts
             (mk_names "x" (length Ts) ~~ Ts))
         in
-          (name_mx, ((Name.no_binding, []), fold_rev lambda (params @ xs)
+          (name_mx, (Attrib.no_binding, fold_rev lambda (params @ xs)
             (list_comb (rec_const, params @ make_bool_args' bs i @
               make_args argTs (xs ~~ Ts)))))
         end) (cnames_syn ~~ cs);
@@ -726,7 +723,7 @@
 
 type add_ind_def =
   inductive_flags ->
-  term list -> ((Name.binding * Attrib.src list) * term) list -> thm list ->
+  term list -> (Attrib.binding * term) list -> thm list ->
   term list -> (Name.binding * mixfix) list ->
   local_theory -> inductive_result * local_theory
 
diff -r 103d9282a946 -r a05ca48ef263 src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -14,11 +14,13 @@
   val add_inductive_i:
     InductivePackage.inductive_flags ->
     ((Name.binding * typ) * mixfix) list ->
-    (string * typ) list -> ((Name.binding * Attrib.src list) * term) list -> thm list ->
-      local_theory -> InductivePackage.inductive_result * local_theory
-  val add_inductive: bool -> bool -> (Name.binding * string option * mixfix) list ->
+    (string * typ) list ->
+    (Attrib.binding * term) list -> thm list ->
+    local_theory -> InductivePackage.inductive_result * local_theory
+  val add_inductive: bool -> bool ->
     (Name.binding * string option * mixfix) list ->
-    ((Name.binding * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
+    (Name.binding * string option * mixfix) list ->
+    (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
     local_theory -> InductivePackage.inductive_result * local_theory
   val setup: theory -> theory
 end;
@@ -471,7 +473,7 @@
 
     (* define inductive sets using previously defined predicates *)
     val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
-      (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, ((Name.no_binding, []),
+      (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.no_binding,
          fold_rev lambda params (HOLogic.Collect_const U $
            HOLogic.ap_split' fs U HOLogic.boolT (list_comb (p, params3))))))
          (cnames_syn ~~ cs_info ~~ preds)) ctxt1;
diff -r 103d9282a946 -r a05ca48ef263 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -9,12 +9,12 @@
 signature PRIMREC_PACKAGE =
 sig
   val add_primrec: (Name.binding * typ option * mixfix) list ->
-    ((Name.binding * Attrib.src list) * term) list -> local_theory -> thm list * local_theory
+    (Attrib.binding * term) list -> local_theory -> thm list * local_theory
   val add_primrec_global: (Name.binding * typ option * mixfix) list ->
-    ((Name.binding * Attrib.src list) * term) list -> theory -> thm list * theory
+    (Attrib.binding * term) list -> theory -> thm list * theory
   val add_primrec_overloaded: (string * (string * typ) * bool) list ->
     (Name.binding * typ option * mixfix) list ->
-    ((Name.binding * Attrib.src list) * term) list -> theory -> thm list * theory
+    (Attrib.binding * term) list -> theory -> thm list * theory
 end;
 
 structure PrimrecPackage : PRIMREC_PACKAGE =
diff -r 103d9282a946 -r a05ca48ef263 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -269,7 +269,7 @@
         " in recdef definition of " ^ quote name);
   in
     Specification.theorem Thm.internalK NONE (K I) (Name.binding bname, atts)
-      [] (Element.Shows [((Name.no_binding, []), [(HOLogic.mk_Trueprop tc, [])])]) int lthy
+      [] (Element.Shows [(Attrib.no_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
   end;
 
 val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const;
diff -r 103d9282a946 -r a05ca48ef263 src/HOL/Tools/typecopy_package.ML
--- a/src/HOL/Tools/typecopy_package.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOL/Tools/typecopy_package.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -134,7 +134,7 @@
           (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
         val def' = Syntax.check_term lthy def;
         val ((_, (_, thm)), lthy') = Specification.definition
-          (NONE, ((Name.no_binding, []), def')) lthy;
+          (NONE, (Attrib.no_binding, def')) lthy;
         val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
         val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
       in (thm', lthy') end;
diff -r 103d9282a946 -r a05ca48ef263 src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOL/Typedef.thy	Tue Sep 02 16:55:33 2008 +0200
@@ -145,7 +145,7 @@
     thy
     |> TheoryTarget.instantiation ([tyco], vs, @{sort itself})
     |> `(fn lthy => Syntax.check_term lthy eq)
-    |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
+    |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
     |> snd
     |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
     |> LocalTheory.exit
diff -r 103d9282a946 -r a05ca48ef263 src/HOL/ex/Quickcheck.thy
--- a/src/HOL/ex/Quickcheck.thy	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOL/ex/Quickcheck.thy	Tue Sep 02 16:55:33 2008 +0200
@@ -132,7 +132,7 @@
                  (map (fn eq => ((Name.no_binding, [del_func]), eq)) eqs')
           |-> add_code
           |> `(fn lthy => Syntax.check_term lthy eq)
-          |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
+          |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
           |> snd
           |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
           |> LocalTheory.exit
@@ -261,7 +261,7 @@
   in
     thy
     |> TheoryTarget.init NONE
-    |> Specification.definition (NONE, ((Name.no_binding, []), eq))
+    |> Specification.definition (NONE, (Attrib.no_binding, eq))
     |> snd
     |> LocalTheory.exit
     |> ProofContext.theory_of
diff -r 103d9282a946 -r a05ca48ef263 src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -9,9 +9,9 @@
 sig
   val legacy_infer_term: theory -> term -> term
   val legacy_infer_prop: theory -> term -> term
-  val add_fixrec: bool -> ((Name.binding * Attrib.src list) * string) list list -> theory -> theory
+  val add_fixrec: bool -> (Attrib.binding * string) list list -> theory -> theory
   val add_fixrec_i: bool -> ((Name.binding * attribute list) * term) list list -> theory -> theory
-  val add_fixpat: (Name.binding * Attrib.src list) * string list -> theory -> theory
+  val add_fixpat: Attrib.binding * string list -> theory -> theory
   val add_fixpat_i: (Name.binding * attribute list) * term list -> theory -> theory
 end;
 
diff -r 103d9282a946 -r a05ca48ef263 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -8,6 +8,8 @@
 signature ATTRIB =
 sig
   type src = Args.src
+  type binding = Name.binding * src list
+  val no_binding: binding
   val print_attributes: theory -> unit
   val intern: theory -> xstring -> string
   val intern_src: theory -> src -> src
@@ -48,8 +50,15 @@
 structure T = OuterLex;
 structure P = OuterParse;
 
+
+(* source and bindings *)
+
 type src = Args.src;
 
+type binding = Name.binding * src list;
+val no_binding: binding = (Name.no_binding, []);
+
+
 
 (** named attributes **)
 
diff -r 103d9282a946 -r a05ca48ef263 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/Pure/Isar/class.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -19,7 +19,7 @@
   val abbrev: class -> Syntax.mode -> Properties.T
     -> (string * mixfix) * term -> theory -> theory
   val note: class -> string
-    -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list
+    -> (Attrib.binding * (thm list * Attrib.src list) list) list
     -> theory -> (bstring * thm list) list * theory
   val declaration: class -> declaration -> theory -> theory
   val refresh_syntax: class -> Proof.context -> Proof.context
@@ -48,7 +48,7 @@
 
   (*old axclass layer*)
   val axclass_cmd: bstring * xstring list
-    -> ((Name.binding * Attrib.src list) * string list) list
+    -> (Attrib.binding * string list) list
     -> theory -> class * theory
   val classrel_cmd: xstring * xstring -> theory -> Proof.state
 
@@ -374,7 +374,7 @@
     thy
     |> fold2 add_constraint (map snd consts) no_constraints
     |> prove_interpretation tac ((false, prfx), []) (Locale.Locale class)
-          (inst, map (fn def => ((Name.no_binding, []), def)) defs)
+          (inst, map (fn def => (Attrib.no_binding, def)) defs)
     |> fold2 add_constraint (map snd consts) constraints
   end;
 
diff -r 103d9282a946 -r a05ca48ef263 src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/Pure/Isar/constdefs.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -11,7 +11,7 @@
 sig
   val add_constdefs: (Name.binding * string option) list *
     ((Name.binding * string option * mixfix) option *
-      ((Name.binding * Attrib.src list) * string)) list -> theory -> theory
+      (Attrib.binding * string)) list -> theory -> theory
   val add_constdefs_i: (Name.binding * typ option) list *
     ((Name.binding * typ option * mixfix) option *
       ((Name.binding * attribute list) * term)) list -> theory -> theory
diff -r 103d9282a946 -r a05ca48ef263 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/Pure/Isar/element.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -9,21 +9,21 @@
 signature ELEMENT =
 sig
   datatype ('typ, 'term) stmt =
-    Shows of ((Name.binding * Attrib.src list) * ('term * 'term list) list) list |
+    Shows of (Attrib.binding * ('term * 'term list) list) list |
     Obtains of (Name.binding * ((Name.binding * 'typ option) list * 'term list)) list
   type statement = (string, string) stmt
   type statement_i = (typ, term) stmt
   datatype ('typ, 'term, 'fact) ctxt =
     Fixes of (Name.binding * 'typ option * mixfix) list |
     Constrains of (string * 'typ) list |
-    Assumes of ((Name.binding * Attrib.src list) * ('term * 'term list) list) list |
-    Defines of ((Name.binding * Attrib.src list) * ('term * 'term list)) list |
-    Notes of string * ((Name.binding * Attrib.src list) * ('fact * Attrib.src list) list) list
+    Assumes of (Attrib.binding * ('term * 'term list) list) list |
+    Defines of (Attrib.binding * ('term * 'term list)) list |
+    Notes of string * (Attrib.binding * ('fact * Attrib.src list) list) list
   type context = (string, string, Facts.ref) ctxt
   type context_i = (typ, term, thm list) ctxt
   val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) ->
-   ((Name.binding * Attrib.src list) * ('fact * Attrib.src list) list) list ->
-   ((Name.binding * Attrib.src list) * ('c * Attrib.src list) list) list
+   (Attrib.binding * ('fact * Attrib.src list) list) list ->
+   (Attrib.binding * ('c * Attrib.src list) list) list
   val map_ctxt: {name: Name.binding -> Name.binding,
     var: Name.binding * mixfix -> Name.binding * mixfix,
     typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
@@ -33,8 +33,7 @@
   val morph_ctxt: morphism -> context_i -> context_i
   val params_of: context_i -> (string * typ) list
   val prems_of: context_i -> term list
-  val facts_of: theory -> context_i ->
-    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list
+  val facts_of: theory -> context_i -> (Attrib.binding * (thm list * Attrib.src list) list) list
   val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
   val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
   val pretty_statement: Proof.context -> string -> thm -> Pretty.T
@@ -71,11 +70,11 @@
   val satisfy_thm: witness list -> thm -> thm
   val satisfy_morphism: witness list -> morphism
   val satisfy_facts: witness list ->
-    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
-    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list
+    (Attrib.binding * (thm list * Attrib.src list) list) list ->
+    (Attrib.binding * (thm list * Attrib.src list) list) list
   val generalize_facts: Proof.context -> Proof.context ->
-    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
-    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list
+    (Attrib.binding * (thm list * Attrib.src list) list) list ->
+    (Attrib.binding * (thm list * Attrib.src list) list) list
 end;
 
 structure Element: ELEMENT =
@@ -86,7 +85,7 @@
 (* statement *)
 
 datatype ('typ, 'term) stmt =
-  Shows of ((Name.binding * Attrib.src list) * ('term * 'term list) list) list |
+  Shows of (Attrib.binding * ('term * 'term list) list) list |
   Obtains of (Name.binding * ((Name.binding * 'typ option) list * 'term list)) list;
 
 type statement = (string, string) stmt;
@@ -98,9 +97,9 @@
 datatype ('typ, 'term, 'fact) ctxt =
   Fixes of (Name.binding * 'typ option * mixfix) list |
   Constrains of (string * 'typ) list |
-  Assumes of ((Name.binding * Attrib.src list) * ('term * 'term list) list) list |
-  Defines of ((Name.binding * Attrib.src list) * ('term * 'term list)) list |
-  Notes of string * ((Name.binding * Attrib.src list) * ('fact * Attrib.src list) list) list;
+  Assumes of (Attrib.binding * ('term * 'term list) list) list |
+  Defines of (Attrib.binding * ('term * 'term list)) list |
+  Notes of string * (Attrib.binding * ('fact * Attrib.src list) list) list;
 
 type context = (string, string, Facts.ref) ctxt;
 type context_i = (typ, term, thm list) ctxt;
@@ -272,8 +271,8 @@
       is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
   in
     pretty_ctxt ctxt' (Fixes (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) fixes)) @
-    pretty_ctxt ctxt' (Assumes (map (fn t => ((Name.no_binding, []), [(t, [])])) assumes)) @
-     (if null cases then pretty_stmt ctxt' (Shows [((Name.no_binding, []), [(concl, [])])])
+    pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.no_binding, [(t, [])])) assumes)) @
+     (if null cases then pretty_stmt ctxt' (Shows [(Attrib.no_binding, [(concl, [])])])
       else
         let val (clauses, ctxt'') = fold_map (obtain o cert) cases ctxt'
         in pretty_stmt ctxt'' (Obtains clauses) end)
diff -r 103d9282a946 -r a05ca48ef263 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -21,14 +21,10 @@
   val simproc_setup: string -> string list -> string * Position.T -> string list ->
     local_theory -> local_theory
   val hide_names: bool -> string * xstring list -> theory -> theory
-  val have: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
-    bool -> Proof.state -> Proof.state
-  val hence: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
-    bool -> Proof.state -> Proof.state
-  val show: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
-    bool -> Proof.state -> Proof.state
-  val thus: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
-    bool -> Proof.state -> Proof.state
+  val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
+  val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
+  val show: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
+  val thus: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
   val terminal_proof: Method.text * Method.text option ->
     Toplevel.transition -> Toplevel.transition
diff -r 103d9282a946 -r a05ca48ef263 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -272,7 +272,7 @@
 val _ =
   OuterSyntax.local_theory "declare" "declare theorems (improper)" K.thy_decl
     (P.and_list1 SpecParse.xthms1
-      >> (fn args => #2 o Specification.theorems_cmd "" [((Name.no_binding, []), flat args)]));
+      >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.no_binding, flat args)]));
 
 
 (* name space entry path *)
@@ -468,7 +468,7 @@
 fun gen_theorem kind =
   OuterSyntax.local_theory_to_proof' kind ("state " ^ kind) K.thy_goal
     (Scan.optional (SpecParse.opt_thm_name ":" --|
-      Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) (Name.no_binding, []) --
+      Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) Attrib.no_binding --
       SpecParse.general_statement >> (fn (a, (elems, concl)) =>
         (Specification.theorem_cmd kind NONE (K I) a elems concl)));
 
diff -r 103d9282a946 -r a05ca48ef263 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/Pure/Isar/local_theory.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -26,15 +26,14 @@
   val affirm: local_theory -> local_theory
   val pretty: local_theory -> Pretty.T list
   val axioms: string ->
-    ((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list -> local_theory
+    ((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list -> local_theory
     -> (term list * (string * thm list) list) * local_theory
   val abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
-  val define: string -> (Name.binding * mixfix) * ((Name.binding * Attrib.src list) * term) -> local_theory ->
+  val define: string -> (Name.binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
-  val note: string -> (Name.binding * Attrib.src list) * thm list ->
-    local_theory -> (string * thm list) * local_theory
-  val notes: string -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
+  val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
+  val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
     local_theory -> (string * thm list) list * local_theory
   val type_syntax: declaration -> local_theory -> local_theory
   val term_syntax: declaration -> local_theory -> local_theory
@@ -57,14 +56,15 @@
 type operations =
  {pretty: local_theory -> Pretty.T list,
   axioms: string ->
-    ((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list -> local_theory
-    -> (term list * (string * thm list) list) * local_theory,
-  abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory -> (term * term) * local_theory,
+    ((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list -> local_theory ->
+    (term list * (string * thm list) list) * local_theory,
+  abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
+    (term * term) * local_theory,
   define: string ->
-    (Name.binding * mixfix) * ((Name.binding * Attrib.src list) * term) -> local_theory ->
+    (Name.binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory,
   notes: string ->
-    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
+    (Attrib.binding * (thm list * Attrib.src list) list) list ->
     local_theory -> (string * thm list) list * local_theory,
   type_syntax: declaration -> local_theory -> local_theory,
   term_syntax: declaration -> local_theory -> local_theory,
diff -r 103d9282a946 -r a05ca48ef263 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -50,21 +50,16 @@
   val init: string -> theory -> Proof.context
 
   (* The specification of a locale *)
-  val parameters_of: theory -> string ->
-    ((string * typ) * mixfix) list
-  val parameters_of_expr: theory -> expr ->
-    ((string * typ) * mixfix) list
-  val local_asms_of: theory -> string ->
-    ((Name.binding * Attrib.src list) * term list) list
-  val global_asms_of: theory -> string ->
-    ((Name.binding * Attrib.src list) * term list) list
+  val parameters_of: theory -> string -> ((string * typ) * mixfix) list
+  val parameters_of_expr: theory -> expr -> ((string * typ) * mixfix) list
+  val local_asms_of: theory -> string -> (Attrib.binding * term list) list
+  val global_asms_of: theory -> string -> (Attrib.binding * term list) list
 
   (* Theorems *)
   val intros: theory -> string -> thm list * thm list
   val dests: theory -> string -> thm list
   (* Not part of the official interface.  DO NOT USE *)
-  val facts_of: theory -> string
-    -> ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list list
+  val facts_of: theory -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list list
 
   (* Processing of locale statements *)
   val read_context_statement: xstring option -> Element.context element list ->
@@ -95,8 +90,7 @@
   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
 
   (* Storing results *)
-  val add_thmss: string -> string ->
-    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
+  val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
     Proof.context -> Proof.context
   val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
   val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
@@ -104,21 +98,21 @@
 
   val interpretation_i: (Proof.context -> Proof.context) ->
     (bool * string) * Attrib.src list -> expr ->
-    term option list * ((Name.binding * Attrib.src list) * term) list ->
+    term option list * (Attrib.binding * term) list ->
     theory -> Proof.state
   val interpretation: (Proof.context -> Proof.context) ->
     (bool * string) * Attrib.src list -> expr ->
-    string option list * ((Name.binding * Attrib.src list) * string) list ->
+    string option list * (Attrib.binding * string) list ->
     theory -> Proof.state
   val interpretation_in_locale: (Proof.context -> Proof.context) ->
     xstring * expr -> theory -> Proof.state
   val interpret_i: (Proof.state -> Proof.state Seq.seq) ->
     (bool * string) * Attrib.src list -> expr ->
-    term option list * ((Name.binding * Attrib.src list) * term) list ->
+    term option list * (Attrib.binding * term) list ->
     bool -> Proof.state -> Proof.state
   val interpret: (Proof.state -> Proof.state Seq.seq) ->
     (bool * string) * Attrib.src list -> expr ->
-    string option list * ((Name.binding * Attrib.src list) * string) list ->
+    string option list * (Attrib.binding * string) list ->
     bool -> Proof.state -> Proof.state
 end;
 
@@ -1275,8 +1269,7 @@
     list_ord (fn ((_, (d1, _)), (_, (d2, _))) =>
       Term.fast_term_ord (d1, d2)) (defs1, defs2);
 structure Defstab =
-    TableFun(type key = ((Name.binding * Attrib.src list) * (term * term list)) list
-        val ord = defs_ord);
+    TableFun(type key = (Attrib.binding * (term * term list)) list val ord = defs_ord);
 
 fun rem_dup_defs es ds =
     fold_map (fn e as (Defines defs) => (fn ds =>
@@ -1908,7 +1901,7 @@
 
 fun defines_to_notes is_ext thy (Defines defs) defns =
     let
-      val defs' = map (fn (_, (def, _)) => ((Name.no_binding, []), (def, []))) defs
+      val defs' = map (fn (_, (def, _)) => (Attrib.no_binding, (def, []))) defs
       val notes = map (fn (a, (def, _)) =>
         (a, [([assume (cterm_of thy def)], [])])) defs
     in
diff -r 103d9282a946 -r a05ca48ef263 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/Pure/Isar/obtain.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -41,7 +41,7 @@
 sig
   val thatN: string
   val obtain: string -> (Name.binding * string option * mixfix) list ->
-    ((Name.binding * Attrib.src list) * (string * string list) list) list ->
+    (Attrib.binding * (string * string list) list) list ->
     bool -> Proof.state -> Proof.state
   val obtain_i: string -> (Name.binding * typ option * mixfix) list ->
     ((Name.binding * attribute list) * (term * term list) list) list ->
diff -r 103d9282a946 -r a05ca48ef263 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -47,26 +47,23 @@
   val fix: (Name.binding * string option * mixfix) list -> state -> state
   val fix_i: (Name.binding * typ option * mixfix) list -> state -> state
   val assm: Assumption.export ->
-    ((Name.binding * Attrib.src list) * (string * string list) list) list -> state -> state
+    (Attrib.binding * (string * string list) list) list -> state -> state
   val assm_i: Assumption.export ->
     ((Name.binding * attribute list) * (term * term list) list) list -> state -> state
-  val assume: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
-    state -> state
+  val assume: (Attrib.binding * (string * string list) list) list -> state -> state
   val assume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
     state -> state
-  val presume: ((Name.binding * Attrib.src list) * (string * string list) list) list ->
-    state -> state
+  val presume: (Attrib.binding * (string * string list) list) list -> state -> state
   val presume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
     state -> state
-  val def: ((Name.binding * Attrib.src list) *
-    ((Name.binding * mixfix) * (string * string list))) list -> state -> state
+  val def: (Attrib.binding * ((Name.binding * mixfix) * (string * string list))) list ->
+    state -> state
   val def_i: ((Name.binding * attribute list) *
     ((Name.binding * mixfix) * (term * term list))) list -> state -> state
   val chain: state -> state
   val chain_facts: thm list -> state -> state
   val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
-  val note_thmss: ((Name.binding * Attrib.src list) *
-    (Facts.ref * Attrib.src list) list) list -> state -> state
+  val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
   val note_thmss_i: ((Name.binding * attribute list) *
     (thm list * attribute list) list) list -> state -> state
   val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
@@ -109,11 +106,11 @@
   val global_done_proof: state -> context
   val global_skip_proof: bool -> state -> context
   val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
-    ((Name.binding * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
+    (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
     ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
   val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
-    ((Name.binding * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
+    (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
     ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
 end;
diff -r 103d9282a946 -r a05ca48ef263 src/Pure/Isar/spec_parse.ML
--- a/src/Pure/Isar/spec_parse.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/Pure/Isar/spec_parse.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -11,34 +11,31 @@
   val attrib: OuterLex.token list -> Attrib.src * token list
   val attribs: token list -> Attrib.src list * token list
   val opt_attribs: token list -> Attrib.src list * token list
-  val thm_name: string -> token list -> (Name.binding * Attrib.src list) * token list
-  val opt_thm_name: string -> token list -> (Name.binding * Attrib.src list) * token list
-  val spec: token list -> ((Name.binding * Attrib.src list) * string list) * token list
-  val named_spec: token list -> ((Name.binding * Attrib.src list) * string list) * token list
+  val thm_name: string -> token list -> Attrib.binding * token list
+  val opt_thm_name: string -> token list -> Attrib.binding * token list
+  val spec: token list -> (Attrib.binding * string list) * token list
+  val named_spec: token list -> (Attrib.binding * string list) * token list
   val spec_name: token list -> ((Name.binding * string) * Attrib.src list) * token list
   val spec_opt_name: token list -> ((Name.binding * string) * Attrib.src list) * token list
   val xthm: token list -> (Facts.ref * Attrib.src list) * token list
   val xthms1: token list -> (Facts.ref * Attrib.src list) list * token list
   val name_facts: token list ->
-    ((Name.binding * Attrib.src list) * (Facts.ref * Attrib.src list) list) list * token list
+    (Attrib.binding * (Facts.ref * Attrib.src list) list) list * token list
   val locale_mixfix: token list -> mixfix * token list
   val locale_fixes: token list -> (Name.binding * string option * mixfix) list * token list
-  val locale_insts: token list ->
-    (string option list * ((Name.binding * Attrib.src list) * string) list) * token list
+  val locale_insts: token list -> (string option list * (Attrib.binding * string) list) * token list
   val class_expr: token list -> string list * token list
   val locale_expr: token list -> Locale.expr * token list
   val locale_keyword: token list -> string * token list
   val locale_element: token list -> Element.context Locale.element * token list
   val context_element: token list -> Element.context * token list
-  val statement: token list ->
-    ((Name.binding * Attrib.src list) * (string * string list) list) list * token list
+  val statement: token list -> (Attrib.binding * (string * string list) list) list * token list
   val general_statement: token list ->
     (Element.context Locale.element list * Element.statement) * OuterLex.token list
   val statement_keyword: token list -> string * token list
   val specification: token list ->
     (Name.binding *
-      (((Name.binding * Attrib.src list) * string list) list *
-        (Name.binding * string option) list)) list * token list
+      ((Attrib.binding * string list) list * (Name.binding * string option) list)) list * token list
 end;
 
 structure SpecParse: SPEC_PARSE =
@@ -58,7 +55,7 @@
 
 fun opt_thm_name s =
   Scan.optional ((P.binding -- opt_attribs || attribs >> pair Name.no_binding) --| P.$$$ s)
-    (Name.no_binding, []);
+    Attrib.no_binding;
 
 val spec = opt_thm_name ":" -- Scan.repeat1 P.prop;
 val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
diff -r 103d9282a946 -r a05ca48ef263 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/Pure/Isar/specification.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -10,32 +10,28 @@
 sig
   val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
   val check_specification: (Name.binding * typ option * mixfix) list ->
-    ((Name.binding * Attrib.src list) * term list) list list -> Proof.context ->
-    (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
-    Proof.context
+    (Attrib.binding * term list) list list -> Proof.context ->
+    (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   val read_specification: (Name.binding * string option * mixfix) list ->
-    ((Name.binding * Attrib.src list) * string list) list list -> Proof.context ->
-    (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
-    Proof.context
+    (Attrib.binding * string list) list list -> Proof.context ->
+    (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   val check_free_specification: (Name.binding * typ option * mixfix) list ->
-    ((Name.binding * Attrib.src list) * term list) list -> Proof.context ->
-    (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
-    Proof.context
+    (Attrib.binding * term list) list -> Proof.context ->
+    (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   val read_free_specification: (Name.binding * string option * mixfix) list ->
-    ((Name.binding * Attrib.src list) * string list) list -> Proof.context ->
-    (((Name.binding * typ) * mixfix) list * ((Name.binding * Attrib.src list) * term list) list) *
-    Proof.context
+    (Attrib.binding * string list) list -> Proof.context ->
+    (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   val axiomatization: (Name.binding * typ option * mixfix) list ->
-    ((Name.binding * Attrib.src list) * term list) list -> local_theory ->
+    (Attrib.binding * term list) list -> local_theory ->
     (term list * (string * thm list) list) * local_theory
   val axiomatization_cmd: (Name.binding * string option * mixfix) list ->
-    ((Name.binding * Attrib.src list) * string list) list -> local_theory ->
+    (Attrib.binding * string list) list -> local_theory ->
     (term list * (string * thm list) list) * local_theory
   val definition:
-    (Name.binding * typ option * mixfix) option * ((Name.binding * Attrib.src list) * term) ->
+    (Name.binding * typ option * mixfix) option * (Attrib.binding * term) ->
     local_theory -> (term * (string * thm)) * local_theory
   val definition_cmd:
-    (Name.binding * string option * mixfix) option * ((Name.binding * Attrib.src list) * string) ->
+    (Name.binding * string option * mixfix) option * (Attrib.binding * string) ->
     local_theory -> (term * (string * thm)) * local_theory
   val abbreviation: Syntax.mode -> (Name.binding * typ option * mixfix) option * term ->
     local_theory -> local_theory
@@ -44,17 +40,17 @@
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   val theorems: string ->
-    ((Name.binding * Attrib.src list) * (thm list * Attrib.src list) list) list ->
+    (Attrib.binding * (thm list * Attrib.src list) list) list ->
     local_theory -> (string * thm list) list * local_theory
   val theorems_cmd: string ->
-    ((Name.binding * Attrib.src list) * (Facts.ref * Attrib.src list) list) list ->
+    (Attrib.binding * (Facts.ref * Attrib.src list) list) list ->
     local_theory -> (string * thm list) list * local_theory
   val theorem: string -> Method.text option ->
-    (thm list list -> local_theory -> local_theory) -> Name.binding * Attrib.src list ->
+    (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
     Element.context_i Locale.element list -> Element.statement_i ->
     bool -> local_theory -> Proof.state
   val theorem_cmd: string -> Method.text option ->
-    (thm list list -> local_theory -> local_theory) -> Name.binding * Attrib.src list ->
+    (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
     Element.context Locale.element list -> Element.statement ->
     bool -> local_theory -> Proof.state
   val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
diff -r 103d9282a946 -r a05ca48ef263 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/Pure/Isar/theory_target.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -51,7 +51,7 @@
     val fixes = map (fn (x, T) =>
       (Name.binding x, SOME T, NoSyn)) (#1 (ProofContext.inferred_fixes ctxt));
     val assumes = map (fn A =>
-      ((Name.no_binding, []), [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
+      (Attrib.no_binding, [(A, [])])) (map Thm.term_of (Assumption.assms_of ctxt));
     val elems =
       (if null fixes then [] else [Element.Fixes fixes]) @
       (if null assumes then [] else [Element.Assumes assumes]);
diff -r 103d9282a946 -r a05ca48ef263 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Tue Sep 02 16:55:33 2008 +0200
@@ -8,7 +8,7 @@
 signature IND_CASES =
 sig
   val declare: string -> (simpset -> cterm -> thm) -> theory -> theory
-  val inductive_cases: ((Name.binding * Attrib.src list) * string list) list -> theory -> theory
+  val inductive_cases: (Attrib.binding * string list) list -> theory -> theory
   val setup: theory -> theory
 end;