cleaned up binding module and related code
authorhaftmann
Thu Dec 04 14:43:33 2008 +0100 (2008-12-04)
changeset 289651de908189869
parent 28963 f6d9e0e0b153
child 28966 71a7f76b522d
cleaned up binding module and related code
NEWS
src/HOL/Code_Eval.thy
src/HOL/Import/hol4rews.ML
src/HOL/Import/proof_kernel.ML
src/HOL/List.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_induct.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_core.ML
src/HOL/Tools/function_package/fundef_lib.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/inductive_wrap.ML
src/HOL/Tools/function_package/mutual.ML
src/HOL/Tools/function_package/size.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/inductive_set_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/typecopy_package.ML
src/HOL/Tools/typedef_package.ML
src/HOL/Typedef.thy
src/HOL/Typerep.thy
src/HOL/ex/Quickcheck.thy
src/HOL/ex/Term_Of_Syntax.thy
src/HOLCF/Tools/domain/domain_axioms.ML
src/HOLCF/Tools/domain/domain_extender.ML
src/HOLCF/Tools/domain/domain_theorems.ML
src/HOLCF/Tools/fixrec_package.ML
src/HOLCF/Tools/pcpodef_package.ML
src/Pure/General/binding.ML
src/Pure/General/name_space.ML
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/class.ML
src/Pure/Isar/constdefs.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/new_locale.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/rule_insts.ML
src/Pure/Isar/spec_parse.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/theory_target.ML
src/Pure/ROOT.ML
src/Pure/Tools/invoke.ML
src/Pure/assumption.ML
src/Pure/axclass.ML
src/Pure/consts.ML
src/Pure/facts.ML
src/Pure/more_thm.ML
src/Pure/morphism.ML
src/Pure/name.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
src/Pure/simplifier.ML
src/Pure/theory.ML
src/Pure/thm.ML
src/Pure/type.ML
src/Pure/variable.ML
src/Tools/induct.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
src/ZF/ind_syntax.ML
     1.1 --- a/NEWS	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/NEWS	Thu Dec 04 14:43:33 2008 +0100
     1.3 @@ -58,6 +58,18 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Type Binding.T gradually replaces formerly used type bstring for names
     1.8 +to be bound.  Name space interface for declarations has been simplified:
     1.9 +
    1.10 +  NameSpace.declare: NameSpace.naming
    1.11 +    -> Binding.T -> NameSpace.T -> string * NameSpace.T
    1.12 +  NameSpace.bind: NameSpace.naming
    1.13 +    -> Binding.T * 'a -> 'a NameSpace.table -> string * 'a NameSpace.table
    1.14 +         (*exception Symtab.DUP*)
    1.15 +
    1.16 +See further modules src/Pure/General/binding.ML and
    1.17 +src/Pure/General/name_space.ML
    1.18 +
    1.19  * Module moves in repository:
    1.20      src/Pure/Tools/value.ML ~> src/Tools/
    1.21      src/Pure/Tools/quickcheck.ML ~> src/Tools/
     2.1 --- a/src/HOL/Code_Eval.thy	Wed Dec 03 21:00:39 2008 -0800
     2.2 +++ b/src/HOL/Code_Eval.thy	Thu Dec 04 14:43:33 2008 +0100
     2.3 @@ -63,7 +63,7 @@
     2.4        thy
     2.5        |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
     2.6        |> `(fn lthy => Syntax.check_term lthy eq)
     2.7 -      |-> (fn eq => Specification.definition (NONE, ((Name.binding (triv_name_of eq), []), eq)))
     2.8 +      |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
     2.9        |> snd
    2.10        |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    2.11        |> LocalTheory.exit_global
     3.1 --- a/src/HOL/Import/hol4rews.ML	Wed Dec 03 21:00:39 2008 -0800
     3.2 +++ b/src/HOL/Import/hol4rews.ML	Thu Dec 04 14:43:33 2008 +0100
     3.3 @@ -282,7 +282,7 @@
     3.4  	val thy = case opt_get_output_thy thy of
     3.5  		      "" => thy
     3.6  		    | output_thy => if internal
     3.7 -				    then add_hol4_cmove (Sign.full_name thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
     3.8 +				    then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
     3.9  				    else thy
    3.10  	val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
    3.11  	val curmaps = HOL4ConstMaps.get thy
    3.12 @@ -324,7 +324,7 @@
    3.13  	val thy = case opt_get_output_thy thy of
    3.14  		      "" => thy
    3.15  		    | output_thy => if internal
    3.16 -				    then add_hol4_cmove (Sign.full_name thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
    3.17 +				    then add_hol4_cmove (Sign.full_bname thy bconst) (output_thy ^ "." ^ bthy ^ "." ^ bconst) thy
    3.18  				    else thy
    3.19  	val _ = message ("Adding cmap " ^ bthy ^ "." ^ bconst ^ " -> " ^ isaconst ^ (if internal then " (*)" else ""))
    3.20  	val curmaps = HOL4ConstMaps.get thy
    3.21 @@ -348,7 +348,7 @@
    3.22  
    3.23  fun add_hol4_pending bthy bthm hth thy =
    3.24      let
    3.25 -	val thmname = Sign.full_name thy bthm
    3.26 +	val thmname = Sign.full_bname thy bthm
    3.27  	val _ = message ("Add pending " ^ bthy ^ "." ^ bthm)
    3.28  	val curpend = HOL4Pending.get thy
    3.29  	val newpend = StringPair.update_new ((bthy,bthm),hth) curpend
     4.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Dec 03 21:00:39 2008 -0800
     4.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Dec 04 14:43:33 2008 +0100
     4.3 @@ -1960,7 +1960,7 @@
     4.4          val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
     4.5                        SOME (_,res) => HOLThm(rens_of linfo,res)
     4.6                      | NONE => raise ERR "new_definition" "Bad conclusion"
     4.7 -        val fullname = Sign.full_name thy22 thmname
     4.8 +        val fullname = Sign.full_bname thy22 thmname
     4.9          val thy22' = case opt_get_output_thy thy22 of
    4.10                           "" => (ImportRecorder.add_hol_mapping thyname thmname fullname;
    4.11                                  add_hol4_mapping thyname thmname fullname thy22)
     5.1 --- a/src/HOL/List.thy	Wed Dec 03 21:00:39 2008 -0800
     5.2 +++ b/src/HOL/List.thy	Thu Dec 04 14:43:33 2008 +0100
     5.3 @@ -3423,7 +3423,7 @@
     5.4     (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
     5.5        nibbles nibbles;
     5.6  in
     5.7 -  PureThy.note_thmss Thm.lemmaK [((Name.binding "nibble_pair_of_char_simps", []), [(thms, [])])]
     5.8 +  PureThy.note_thmss Thm.lemmaK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
     5.9    #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
    5.10  end
    5.11  *}
     6.1 --- a/src/HOL/Nominal/Nominal.thy	Wed Dec 03 21:00:39 2008 -0800
     6.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Dec 04 14:43:33 2008 +0100
     6.3 @@ -1,5 +1,3 @@
     6.4 -(* $Id$ *)
     6.5 -
     6.6  theory Nominal 
     6.7  imports Main Infinite_Set
     6.8  uses
     7.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Dec 03 21:00:39 2008 -0800
     7.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Dec 04 14:43:33 2008 +0100
     7.3 @@ -170,7 +170,7 @@
     7.4      val (swap_eqs, thy3) = fold_map (fn (ak_name, T) => fn thy =>
     7.5        let
     7.6          val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
     7.7 -        val swap_name = Sign.full_name thy ("swap_" ^ ak_name);
     7.8 +        val swap_name = Sign.full_bname thy ("swap_" ^ ak_name);
     7.9          val a = Free ("a", T);
    7.10          val b = Free ("b", T);
    7.11          val c = Free ("c", T);
    7.12 @@ -199,10 +199,10 @@
    7.13      val (prm_eqs, thy4) = fold_map (fn (ak_name, T) => fn thy =>
    7.14        let
    7.15          val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
    7.16 -        val swap_name = Sign.full_name thy ("swap_" ^ ak_name)
    7.17 +        val swap_name = Sign.full_bname thy ("swap_" ^ ak_name)
    7.18          val prmT = mk_permT T --> T --> T;
    7.19          val prm_name = ak_name ^ "_prm_" ^ ak_name;
    7.20 -        val qu_prm_name = Sign.full_name thy prm_name;
    7.21 +        val qu_prm_name = Sign.full_bname thy prm_name;
    7.22          val x  = Free ("x", HOLogic.mk_prodT (T, T));
    7.23          val xs = Free ("xs", mk_permT T);
    7.24          val a  = Free ("a", T) ;
    7.25 @@ -235,7 +235,7 @@
    7.26            val pi = Free ("pi", mk_permT T);
    7.27            val a  = Free ("a", T');
    7.28            val cperm = Const ("Nominal.perm", mk_permT T --> T' --> T');
    7.29 -          val cperm_def = Const (Sign.full_name thy' perm_def_name, mk_permT T --> T' --> T');
    7.30 +          val cperm_def = Const (Sign.full_bname thy' perm_def_name, mk_permT T --> T' --> T');
    7.31  
    7.32            val name = ak_name ^ "_prm_" ^ ak_name' ^ "_def";
    7.33            val def = Logic.mk_equals
    7.34 @@ -250,7 +250,7 @@
    7.35      val (prm_cons_thms,thy6) = 
    7.36        thy5 |> PureThy.add_thms (map (fn (ak_name, T) =>
    7.37        let
    7.38 -        val ak_name_qu = Sign.full_name thy5 (ak_name);
    7.39 +        val ak_name_qu = Sign.full_bname thy5 (ak_name);
    7.40          val i_type = Type(ak_name_qu,[]);
    7.41          val cat = Const ("Nominal.at",(Term.itselfT i_type)  --> HOLogic.boolT);
    7.42          val at_type = Logic.mk_type i_type;
    7.43 @@ -299,9 +299,9 @@
    7.44                          HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
    7.45        in
    7.46            AxClass.define_class (cl_name, ["HOL.type"]) []
    7.47 -                [((Name.binding (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
    7.48 -                 ((Name.binding (cl_name ^ "2"), []), [axiom2]),                           
    7.49 -                 ((Name.binding (cl_name ^ "3"), []), [axiom3])] thy
    7.50 +                [((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
    7.51 +                 ((Binding.name (cl_name ^ "2"), []), [axiom2]),                           
    7.52 +                 ((Binding.name (cl_name ^ "3"), []), [axiom3])] thy
    7.53        end) ak_names_types thy6;
    7.54  
    7.55      (* proves that every pt_<ak>-type together with <ak>-type *)
    7.56 @@ -311,8 +311,8 @@
    7.57      val (prm_inst_thms,thy8) = 
    7.58        thy7 |> PureThy.add_thms (map (fn (ak_name, T) =>
    7.59        let
    7.60 -        val ak_name_qu = Sign.full_name thy7 ak_name;
    7.61 -        val pt_name_qu = Sign.full_name thy7 ("pt_"^ak_name);
    7.62 +        val ak_name_qu = Sign.full_bname thy7 ak_name;
    7.63 +        val pt_name_qu = Sign.full_bname thy7 ("pt_"^ak_name);
    7.64          val i_type1 = TFree("'x",[pt_name_qu]);
    7.65          val i_type2 = Type(ak_name_qu,[]);
    7.66          val cpt = Const ("Nominal.pt",(Term.itselfT i_type1)-->(Term.itselfT i_type2)-->HOLogic.boolT);
    7.67 @@ -338,7 +338,7 @@
    7.68       val (fs_ax_classes,thy11) =  fold_map (fn (ak_name, T) => fn thy =>
    7.69         let 
    7.70            val cl_name = "fs_"^ak_name;
    7.71 -          val pt_name = Sign.full_name thy ("pt_"^ak_name);
    7.72 +          val pt_name = Sign.full_bname thy ("pt_"^ak_name);
    7.73            val ty = TFree("'a",["HOL.type"]);
    7.74            val x   = Free ("x", ty);
    7.75            val csupp    = Const ("Nominal.supp", ty --> HOLogic.mk_setT T);
    7.76 @@ -347,7 +347,7 @@
    7.77            val axiom1   = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
    7.78  
    7.79         in  
    7.80 -        AxClass.define_class (cl_name, [pt_name]) [] [((Name.binding (cl_name ^ "1"), []), [axiom1])] thy            
    7.81 +        AxClass.define_class (cl_name, [pt_name]) [] [((Binding.name (cl_name ^ "1"), []), [axiom1])] thy            
    7.82         end) ak_names_types thy8; 
    7.83           
    7.84       (* proves that every fs_<ak>-type together with <ak>-type   *)
    7.85 @@ -357,8 +357,8 @@
    7.86       val (fs_inst_thms,thy12) = 
    7.87         thy11 |> PureThy.add_thms (map (fn (ak_name, T) =>
    7.88         let
    7.89 -         val ak_name_qu = Sign.full_name thy11 ak_name;
    7.90 -         val fs_name_qu = Sign.full_name thy11 ("fs_"^ak_name);
    7.91 +         val ak_name_qu = Sign.full_bname thy11 ak_name;
    7.92 +         val fs_name_qu = Sign.full_bname thy11 ("fs_"^ak_name);
    7.93           val i_type1 = TFree("'x",[fs_name_qu]);
    7.94           val i_type2 = Type(ak_name_qu,[]);
    7.95           val cfs = Const ("Nominal.fs", 
    7.96 @@ -397,7 +397,7 @@
    7.97                                             cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
    7.98                 in  
    7.99                   AxClass.define_class (cl_name, ["HOL.type"]) []
   7.100 -                   [((Name.binding (cl_name ^ "1"), []), [ax1])] thy'  
   7.101 +                   [((Binding.name (cl_name ^ "1"), []), [ax1])] thy'  
   7.102                 end) ak_names_types thy) ak_names_types thy12;
   7.103  
   7.104          (* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem;     *)
   7.105 @@ -406,9 +406,9 @@
   7.106          val (cp_thms,thy12c) = fold_map (fn (ak_name, T) => fn thy =>
   7.107           fold_map (fn (ak_name', T') => fn thy' =>
   7.108             let
   7.109 -             val ak_name_qu  = Sign.full_name thy' (ak_name);
   7.110 -             val ak_name_qu' = Sign.full_name thy' (ak_name');
   7.111 -             val cp_name_qu  = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name');
   7.112 +             val ak_name_qu  = Sign.full_bname thy' (ak_name);
   7.113 +             val ak_name_qu' = Sign.full_bname thy' (ak_name');
   7.114 +             val cp_name_qu  = Sign.full_bname thy' ("cp_"^ak_name^"_"^ak_name');
   7.115               val i_type0 = TFree("'a",[cp_name_qu]);
   7.116               val i_type1 = Type(ak_name_qu,[]);
   7.117               val i_type2 = Type(ak_name_qu',[]);
   7.118 @@ -442,8 +442,8 @@
   7.119            (if not (ak_name = ak_name') 
   7.120             then 
   7.121                 let
   7.122 -                 val ak_name_qu  = Sign.full_name thy' ak_name;
   7.123 -                 val ak_name_qu' = Sign.full_name thy' ak_name';
   7.124 +                 val ak_name_qu  = Sign.full_bname thy' ak_name;
   7.125 +                 val ak_name_qu' = Sign.full_bname thy' ak_name';
   7.126                   val i_type1 = Type(ak_name_qu,[]);
   7.127                   val i_type2 = Type(ak_name_qu',[]);
   7.128                   val cdj = Const ("Nominal.disjoint",
   7.129 @@ -487,8 +487,8 @@
   7.130       val thy13 = fold (fn ak_name => fn thy =>
   7.131          fold (fn ak_name' => fn thy' =>
   7.132           let
   7.133 -           val qu_name =  Sign.full_name thy' ak_name';
   7.134 -           val cls_name = Sign.full_name thy' ("pt_"^ak_name);
   7.135 +           val qu_name =  Sign.full_bname thy' ak_name';
   7.136 +           val cls_name = Sign.full_bname thy' ("pt_"^ak_name);
   7.137             val at_inst  = PureThy.get_thm thy' ("at_" ^ ak_name' ^ "_inst");
   7.138  
   7.139             val proof1 = EVERY [Class.intro_classes_tac [],
   7.140 @@ -518,7 +518,7 @@
   7.141       (* are instances of pt_<ak>        *)
   7.142       val thy18 = fold (fn ak_name => fn thy =>
   7.143         let
   7.144 -          val cls_name = Sign.full_name thy ("pt_"^ak_name);
   7.145 +          val cls_name = Sign.full_bname thy ("pt_"^ak_name);
   7.146            val at_thm   = PureThy.get_thm thy ("at_"^ak_name^"_inst");
   7.147            val pt_inst  = PureThy.get_thm thy ("pt_"^ak_name^"_inst");
   7.148  
   7.149 @@ -562,8 +562,8 @@
   7.150         val thy20 = fold (fn ak_name => fn thy =>
   7.151          fold (fn ak_name' => fn thy' =>
   7.152          let
   7.153 -           val qu_name =  Sign.full_name thy' ak_name';
   7.154 -           val qu_class = Sign.full_name thy' ("fs_"^ak_name);
   7.155 +           val qu_name =  Sign.full_bname thy' ak_name';
   7.156 +           val qu_class = Sign.full_bname thy' ("fs_"^ak_name);
   7.157             val proof =
   7.158                 (if ak_name = ak_name'
   7.159                  then
   7.160 @@ -588,7 +588,7 @@
   7.161  
   7.162         val thy24 = fold (fn ak_name => fn thy => 
   7.163          let
   7.164 -          val cls_name = Sign.full_name thy ("fs_"^ak_name);
   7.165 +          val cls_name = Sign.full_bname thy ("fs_"^ak_name);
   7.166            val fs_inst  = PureThy.get_thm thy ("fs_"^ak_name^"_inst");
   7.167            fun fs_proof thm = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1];
   7.168  
   7.169 @@ -628,8 +628,8 @@
   7.170           fold (fn ak_name' => fn thy' =>
   7.171            fold (fn ak_name'' => fn thy'' =>
   7.172              let
   7.173 -              val name =  Sign.full_name thy'' ak_name;
   7.174 -              val cls_name = Sign.full_name thy'' ("cp_"^ak_name'^"_"^ak_name'');
   7.175 +              val name =  Sign.full_bname thy'' ak_name;
   7.176 +              val cls_name = Sign.full_bname thy'' ("cp_"^ak_name'^"_"^ak_name'');
   7.177                val proof =
   7.178                  (if (ak_name'=ak_name'') then 
   7.179                    (let
   7.180 @@ -666,7 +666,7 @@
   7.181         val thy26 = fold (fn ak_name => fn thy =>
   7.182          fold (fn ak_name' => fn thy' =>
   7.183          let
   7.184 -            val cls_name = Sign.full_name thy' ("cp_"^ak_name^"_"^ak_name');
   7.185 +            val cls_name = Sign.full_bname thy' ("cp_"^ak_name^"_"^ak_name');
   7.186              val cp_inst  = PureThy.get_thm thy' ("cp_"^ak_name^"_"^ak_name'^"_inst");
   7.187              val pt_inst  = PureThy.get_thm thy' ("pt_"^ak_name^"_inst");
   7.188              val at_inst  = PureThy.get_thm thy' ("at_"^ak_name^"_inst");
   7.189 @@ -698,7 +698,7 @@
   7.190            fun discrete_pt_inst discrete_ty defn =
   7.191               fold (fn ak_name => fn thy =>
   7.192               let
   7.193 -               val qu_class = Sign.full_name thy ("pt_"^ak_name);
   7.194 +               val qu_class = Sign.full_bname thy ("pt_"^ak_name);
   7.195                 val simp_s = HOL_basic_ss addsimps [defn];
   7.196                 val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
   7.197               in 
   7.198 @@ -708,7 +708,7 @@
   7.199            fun discrete_fs_inst discrete_ty defn = 
   7.200               fold (fn ak_name => fn thy =>
   7.201               let
   7.202 -               val qu_class = Sign.full_name thy ("fs_"^ak_name);
   7.203 +               val qu_class = Sign.full_bname thy ("fs_"^ak_name);
   7.204                 val supp_def = @{thm "Nominal.supp_def"};
   7.205                 val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn];
   7.206                 val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
   7.207 @@ -719,7 +719,7 @@
   7.208            fun discrete_cp_inst discrete_ty defn = 
   7.209               fold (fn ak_name' => (fold (fn ak_name => fn thy =>
   7.210               let
   7.211 -               val qu_class = Sign.full_name thy ("cp_"^ak_name^"_"^ak_name');
   7.212 +               val qu_class = Sign.full_bname thy ("cp_"^ak_name^"_"^ak_name');
   7.213                 val supp_def = @{thm "Nominal.supp_def"};
   7.214                 val simp_s = HOL_ss addsimps [defn];
   7.215                 val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
     8.1 --- a/src/HOL/Nominal/nominal_induct.ML	Wed Dec 03 21:00:39 2008 -0800
     8.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Thu Dec 04 14:43:33 2008 +0100
     8.3 @@ -6,7 +6,7 @@
     8.4  
     8.5  structure NominalInduct:
     8.6  sig
     8.7 -  val nominal_induct_tac: Proof.context -> (Name.binding option * term) option list list ->
     8.8 +  val nominal_induct_tac: Proof.context -> (Binding.T option * term) option list list ->
     8.9      (string * typ) list -> (string * typ) list list -> thm list ->
    8.10      thm list -> int -> RuleCases.cases_tactic
    8.11    val nominal_induct_method: Method.src -> Proof.context -> Method.method
     9.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Dec 03 21:00:39 2008 -0800
     9.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Dec 04 14:43:33 2008 +0100
     9.3 @@ -182,7 +182,7 @@
     9.4      fun mk_avoids params name sets =
     9.5        let
     9.6          val (_, ctxt') = ProofContext.add_fixes_i
     9.7 -          (map (fn (s, T) => (Name.binding s, SOME T, NoSyn)) params) ctxt;
     9.8 +          (map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt;
     9.9          fun mk s =
    9.10            let
    9.11              val t = Syntax.read_term ctxt' s;
    10.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Dec 03 21:00:39 2008 -0800
    10.2 +++ b/src/HOL/Nominal/nominal_package.ML	Thu Dec 04 14:43:33 2008 +0100
    10.3 @@ -227,7 +227,7 @@
    10.4        map (fn (cname, cargs, mx) => (cname, mx)) constrs) dts';
    10.5  
    10.6      val ps = map (fn (_, n, _, _) =>
    10.7 -      (Sign.full_name tmp_thy n, Sign.full_name tmp_thy (n ^ "_Rep"))) dts;
    10.8 +      (Sign.full_bname tmp_thy n, Sign.full_bname tmp_thy (n ^ "_Rep"))) dts;
    10.9      val rps = map Library.swap ps;
   10.10  
   10.11      fun replace_types (Type ("Nominal.ABS", [T, U])) =
   10.12 @@ -241,7 +241,7 @@
   10.13          map replace_types cargs, NoSyn)) constrs)) dts';
   10.14  
   10.15      val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
   10.16 -    val full_new_type_names' = map (Sign.full_name thy) new_type_names';
   10.17 +    val full_new_type_names' = map (Sign.full_bname thy) new_type_names';
   10.18  
   10.19      val ({induction, ...},thy1) =
   10.20        DatatypePackage.add_datatype err flat_names new_type_names' dts'' thy;
   10.21 @@ -263,7 +263,7 @@
   10.22      val perm_names' = DatatypeProp.indexify_names (map (fn (i, _) =>
   10.23        "perm_" ^ name_of_typ (nth_dtyp i)) descr);
   10.24      val perm_names = replicate (length new_type_names) "Nominal.perm" @
   10.25 -      map (Sign.full_name thy1) (List.drop (perm_names', length new_type_names));
   10.26 +      map (Sign.full_bname thy1) (List.drop (perm_names', length new_type_names));
   10.27      val perm_names_types = perm_names ~~ perm_types;
   10.28      val perm_names_types' = perm_names' ~~ perm_types;
   10.29  
   10.30 @@ -289,7 +289,7 @@
   10.31                else Const ("Nominal.perm", permT --> T --> T) $ pi $ x
   10.32              end;
   10.33          in
   10.34 -          (Attrib.no_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
   10.35 +          (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
   10.36              (Free (nth perm_names_types' i) $
   10.37                 Free ("pi", mk_permT (TFree ("'x", HOLogic.typeS))) $
   10.38                 list_comb (c, args),
   10.39 @@ -301,7 +301,7 @@
   10.40        PrimrecPackage.add_primrec_overloaded
   10.41          (map (fn (s, sT) => (s, sT, false))
   10.42             (List.take (perm_names' ~~ perm_names_types, length new_type_names)))
   10.43 -        (map (fn s => (Name.binding s, NONE, NoSyn)) perm_names') perm_eqs thy1;
   10.44 +        (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs thy1;
   10.45  
   10.46      (**** prove that permutation functions introduced by unfolding are ****)
   10.47      (**** equivalent to already existing permutation functions         ****)
   10.48 @@ -566,16 +566,16 @@
   10.49                  (rep_set_name, T))
   10.50                end)
   10.51                  (descr ~~ rep_set_names))));
   10.52 -    val rep_set_names'' = map (Sign.full_name thy3) rep_set_names';
   10.53 +    val rep_set_names'' = map (Sign.full_bname thy3) rep_set_names';
   10.54  
   10.55      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
   10.56          InductivePackage.add_inductive_global (serial_string ())
   10.57            {quiet_mode = false, verbose = false, kind = Thm.internalK,
   10.58 -           alt_name = Name.binding big_rep_name, coind = false, no_elim = true, no_ind = false,
   10.59 +           alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
   10.60             skip_mono = true}
   10.61 -          (map (fn (s, T) => ((Name.binding s, T --> HOLogic.boolT), NoSyn))
   10.62 +          (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
   10.63               (rep_set_names' ~~ recTs'))
   10.64 -          [] (map (fn x => (Attrib.no_binding, x)) intr_ts) [] thy3;
   10.65 +          [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy3;
   10.66  
   10.67      (**** Prove that representing set is closed under permutation ****)
   10.68  
   10.69 @@ -768,7 +768,7 @@
   10.70      val newTs' = Library.take (length new_type_names, recTs');
   10.71      val newTs = Library.take (length new_type_names, recTs);
   10.72  
   10.73 -    val full_new_type_names = map (Sign.full_name thy) new_type_names;
   10.74 +    val full_new_type_names = map (Sign.full_bname thy) new_type_names;
   10.75  
   10.76      fun make_constr_def tname T T' ((thy, defs, eqns),
   10.77          (((cname_rep, _), (cname, cargs)), (cname', mx))) =
   10.78 @@ -1432,7 +1432,7 @@
   10.79        if length descr'' = 1 then [big_rec_name] else
   10.80          map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
   10.81            (1 upto (length descr''));
   10.82 -    val rec_set_names =  map (Sign.full_name thy10) rec_set_names';
   10.83 +    val rec_set_names =  map (Sign.full_bname thy10) rec_set_names';
   10.84  
   10.85      val rec_fns = map (uncurry (mk_Free "f"))
   10.86        (rec_fn_Ts ~~ (1 upto (length rec_fn_Ts)));
   10.87 @@ -1509,12 +1509,12 @@
   10.88        thy10 |>
   10.89          InductivePackage.add_inductive_global (serial_string ())
   10.90            {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
   10.91 -           alt_name = Name.binding big_rec_name, coind = false, no_elim = false, no_ind = false,
   10.92 +           alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
   10.93             skip_mono = true}
   10.94 -          (map (fn (s, T) => ((Name.binding s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
   10.95 +          (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
   10.96            (map dest_Free rec_fns)
   10.97 -          (map (fn x => (Attrib.no_binding, x)) rec_intr_ts) [] ||>
   10.98 -      PureThy.hide_fact true (NameSpace.append (Sign.full_name thy10 big_rec_name) "induct");
   10.99 +          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||>
  10.100 +      PureThy.hide_fact true (NameSpace.append (Sign.full_bname thy10 big_rec_name) "induct");
  10.101  
  10.102      (** equivariance **)
  10.103  
  10.104 @@ -2002,7 +2002,7 @@
  10.105      (* define primrec combinators *)
  10.106  
  10.107      val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
  10.108 -    val reccomb_names = map (Sign.full_name thy11)
  10.109 +    val reccomb_names = map (Sign.full_bname thy11)
  10.110        (if length descr'' = 1 then [big_reccomb_name] else
  10.111          (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
  10.112            (1 upto (length descr''))));
    11.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Wed Dec 03 21:00:39 2008 -0800
    11.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Dec 04 14:43:33 2008 +0100
    11.3 @@ -9,13 +9,13 @@
    11.4  signature NOMINAL_PRIMREC =
    11.5  sig
    11.6    val add_primrec: string -> string list option -> string option ->
    11.7 -    ((Name.binding * string) * Attrib.src list) list -> theory -> Proof.state
    11.8 +    ((Binding.T * string) * Attrib.src list) list -> theory -> Proof.state
    11.9    val add_primrec_unchecked: string -> string list option -> string option ->
   11.10 -    ((Name.binding * string) * Attrib.src list) list -> theory -> Proof.state
   11.11 +    ((Binding.T * string) * Attrib.src list) list -> theory -> Proof.state
   11.12    val add_primrec_i: string -> term list option -> term option ->
   11.13 -    ((Name.binding * term) * attribute list) list -> theory -> Proof.state
   11.14 +    ((Binding.T * term) * attribute list) list -> theory -> Proof.state
   11.15    val add_primrec_unchecked_i: string -> term list option -> term option ->
   11.16 -    ((Name.binding * term) * attribute list) list -> theory -> Proof.state
   11.17 +    ((Binding.T * term) * attribute list) list -> theory -> Proof.state
   11.18  end;
   11.19  
   11.20  structure NominalPrimrec : NOMINAL_PRIMREC =
    12.1 --- a/src/HOL/Statespace/state_space.ML	Wed Dec 03 21:00:39 2008 -0800
    12.2 +++ b/src/HOL/Statespace/state_space.ML	Thu Dec 04 14:43:33 2008 +0100
    12.3 @@ -268,7 +268,7 @@
    12.4                  (map (fn n => Locale.Rename (Locale.Locale (Locale.intern thy "var")
    12.5                                              ,[SOME (n,NONE)])) all_comps);
    12.6  
    12.7 -    val full_name = Sign.full_name thy name;
    12.8 +    val full_name = Sign.full_bname thy name;
    12.9      val dist_thm_name = distinct_compsN;
   12.10      val dist_thm_full_name =
   12.11          let val prefix = fold1' (fn name => fn prfx => prfx ^ "_" ^ name) all_comps "";
   12.12 @@ -302,7 +302,7 @@
   12.13  
   12.14      val attr = Attrib.internal type_attr;
   12.15  
   12.16 -    val assumes = Element.Assumes [((Name.binding dist_thm_name,[attr]),
   12.17 +    val assumes = Element.Assumes [((Binding.name dist_thm_name,[attr]),
   12.18                      [(HOLogic.Trueprop $
   12.19                        (Const ("DistinctTreeProver.all_distinct",
   12.20                                   Type ("DistinctTreeProver.tree",[nameT]) --> HOLogic.boolT) $
   12.21 @@ -373,7 +373,7 @@
   12.22  
   12.23  fun statespace_definition state_type args name parents parent_comps components thy =
   12.24    let
   12.25 -    val full_name = Sign.full_name thy name;
   12.26 +    val full_name = Sign.full_bname thy name;
   12.27      val all_comps = parent_comps @ components;
   12.28  
   12.29      val components' = map (fn (n,T) => (n,(T,full_name))) components;
   12.30 @@ -443,7 +443,7 @@
   12.31           NONE => []
   12.32         | SOME s =>
   12.33            let
   12.34 -	    val fx = Element.Fixes [(Name.binding s,SOME (string_of_typ stateT),NoSyn)];
   12.35 +	    val fx = Element.Fixes [(Binding.name s,SOME (string_of_typ stateT),NoSyn)];
   12.36              val cs = Element.Constrains
   12.37                         (map (fn (n,T) =>  (n,string_of_typ T))
   12.38                           ((map (fn (n,_) => (n,nameT)) all_comps) @
   12.39 @@ -490,7 +490,7 @@
   12.40  
   12.41      fun add_parent (Ts,pname,rs) env =
   12.42        let
   12.43 -        val full_pname = Sign.full_name thy pname;
   12.44 +        val full_pname = Sign.full_bname thy pname;
   12.45          val {args,components,...} =
   12.46                (case get_statespace (Context.Theory thy) full_pname of
   12.47                  SOME r => r
    13.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Wed Dec 03 21:00:39 2008 -0800
    13.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Dec 04 14:43:33 2008 +0100
    13.3 @@ -108,7 +108,7 @@
    13.4        if length descr' = 1 then [big_rec_name'] else
    13.5          map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int)
    13.6            (1 upto (length descr'));
    13.7 -    val rec_set_names = map (Sign.full_name thy0) rec_set_names';
    13.8 +    val rec_set_names = map (Sign.full_bname thy0) rec_set_names';
    13.9  
   13.10      val (rec_result_Ts, reccomb_fn_Ts) = DatatypeProp.make_primrec_Ts descr sorts used;
   13.11  
   13.12 @@ -156,11 +156,11 @@
   13.13      val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
   13.14          InductivePackage.add_inductive_global (serial_string ())
   13.15            {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
   13.16 -            alt_name = Name.binding big_rec_name', coind = false, no_elim = false, no_ind = true,
   13.17 +            alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
   13.18              skip_mono = true}
   13.19 -          (map (fn (s, T) => ((Name.binding s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
   13.20 +          (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
   13.21            (map dest_Free rec_fns)
   13.22 -          (map (fn x => (Attrib.no_binding, x)) rec_intr_ts) [] thy0;
   13.23 +          (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] thy0;
   13.24  
   13.25      (* prove uniqueness and termination of primrec combinators *)
   13.26  
   13.27 @@ -226,7 +226,7 @@
   13.28      (* define primrec combinators *)
   13.29  
   13.30      val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
   13.31 -    val reccomb_names = map (Sign.full_name thy1)
   13.32 +    val reccomb_names = map (Sign.full_bname thy1)
   13.33        (if length descr' = 1 then [big_reccomb_name] else
   13.34          (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
   13.35            (1 upto (length descr'))));
   13.36 @@ -294,7 +294,7 @@
   13.37        in Const (@{const_name undefined}, Ts @ Ts' ---> T')
   13.38        end) constrs) descr';
   13.39  
   13.40 -    val case_names = map (fn s => Sign.full_name thy1 (s ^ "_case")) new_type_names;
   13.41 +    val case_names = map (fn s => Sign.full_bname thy1 (s ^ "_case")) new_type_names;
   13.42  
   13.43      (* define case combinators via primrec combinators *)
   13.44  
   13.45 @@ -317,7 +317,7 @@
   13.46            val fns = (List.concat (Library.take (i, case_dummy_fns))) @
   13.47              fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns)));
   13.48            val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
   13.49 -          val decl = ((Name.binding (Sign.base_name name), caseT), NoSyn);
   13.50 +          val decl = ((Binding.name (Sign.base_name name), caseT), NoSyn);
   13.51            val def = ((Sign.base_name name) ^ "_def",
   13.52              Logic.mk_equals (list_comb (Const (name, caseT), fns1),
   13.53                list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @
    14.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Dec 03 21:00:39 2008 -0800
    14.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Dec 04 14:43:33 2008 +0100
    14.3 @@ -440,7 +440,7 @@
    14.4            (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));
    14.5          val def' = Syntax.check_term lthy def;
    14.6          val ((_, (_, thm)), lthy') = Specification.definition
    14.7 -          (NONE, (Attrib.no_binding, def')) lthy;
    14.8 +          (NONE, (Attrib.empty_binding, def')) lthy;
    14.9          val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
   14.10          val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
   14.11        in (thm', lthy') end;
    15.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Dec 03 21:00:39 2008 -0800
    15.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Dec 04 14:43:33 2008 +0100
    15.3 @@ -567,7 +567,7 @@
    15.4  
    15.5      val (tyvars, _, _, _)::_ = dts;
    15.6      val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
    15.7 -      let val full_tname = Sign.full_name tmp_thy (Syntax.type_name tname mx)
    15.8 +      let val full_tname = Sign.full_bname tmp_thy (Syntax.type_name tname mx)
    15.9        in (case duplicates (op =) tvs of
   15.10              [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
   15.11                    else error ("Mutually recursive datatypes must have same type parameters")
   15.12 @@ -586,8 +586,8 @@
   15.13              val _ = (case fold (curry add_typ_tfree_names) cargs' [] \\ tvs of
   15.14                  [] => ()
   15.15                | vs => error ("Extra type variables on rhs: " ^ commas vs))
   15.16 -          in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
   15.17 -                Sign.full_name_path tmp_thy tname) (Syntax.const_name cname mx'),
   15.18 +          in (constrs @ [((if flat_names then Sign.full_bname tmp_thy else
   15.19 +                Sign.full_bname_path tmp_thy tname) (Syntax.const_name cname mx'),
   15.20                     map (dtyp_of_typ new_dts) cargs')],
   15.21                constr_syntax' @ [(cname, mx')], sorts'')
   15.22            end handle ERROR msg =>
   15.23 @@ -600,7 +600,7 @@
   15.24        in
   15.25          case duplicates (op =) (map fst constrs') of
   15.26             [] =>
   15.27 -             (dts' @ [(i, (Sign.full_name tmp_thy (Syntax.type_name tname mx),
   15.28 +             (dts' @ [(i, (Sign.full_bname tmp_thy (Syntax.type_name tname mx),
   15.29                  map DtTFree tvs, constrs'))],
   15.30                constr_syntax @ [constr_syntax'], sorts', i + 1)
   15.31           | dups => error ("Duplicate constructors " ^ commas dups ^
    16.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Dec 03 21:00:39 2008 -0800
    16.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Dec 04 14:43:33 2008 +0100
    16.3 @@ -77,7 +77,7 @@
    16.4        (if length descr' = 1 then [big_rec_name] else
    16.5          (map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
    16.6            (1 upto (length descr'))));
    16.7 -    val rep_set_names = map (Sign.full_name thy1) rep_set_names';
    16.8 +    val rep_set_names = map (Sign.full_bname thy1) rep_set_names';
    16.9  
   16.10      val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
   16.11      val leafTs' = get_nonrec_types descr' sorts;
   16.12 @@ -184,10 +184,10 @@
   16.13      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
   16.14          InductivePackage.add_inductive_global (serial_string ())
   16.15            {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
   16.16 -           alt_name = Name.binding big_rec_name, coind = false, no_elim = true, no_ind = false,
   16.17 +           alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
   16.18             skip_mono = true}
   16.19 -          (map (fn s => ((Name.binding s, UnivT'), NoSyn)) rep_set_names') []
   16.20 -          (map (fn x => (Attrib.no_binding, x)) intr_ts) [] thy1;
   16.21 +          (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
   16.22 +          (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy1;
   16.23  
   16.24      (********************************* typedef ********************************)
   16.25  
   16.26 @@ -210,7 +210,7 @@
   16.27      val rep_names' = map (fn i => big_rep_name ^ (string_of_int i))
   16.28        (1 upto (length (flat (tl descr))));
   16.29      val all_rep_names = map (Sign.intern_const thy3) rep_names @
   16.30 -      map (Sign.full_name thy3) rep_names';
   16.31 +      map (Sign.full_bname thy3) rep_names';
   16.32  
   16.33      (* isomorphism declarations *)
   16.34  
    17.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Wed Dec 03 21:00:39 2008 -0800
    17.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu Dec 04 14:43:33 2008 +0100
    17.3 @@ -82,7 +82,7 @@
    17.4                                        psimps, pinducts, termination, defname}) phi =
    17.5      let
    17.6        val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
    17.7 -      val name = Name.name_of o Morphism.name phi o Name.binding
    17.8 +      val name = Name.name_of o Morphism.binding phi o Binding.name
    17.9      in
   17.10        FundefCtxData { add_simps = add_simps, case_names = case_names,
   17.11                        fs = map term fs, R = term R, psimps = fact psimps, 
    18.1 --- a/src/HOL/Tools/function_package/fundef_core.ML	Wed Dec 03 21:00:39 2008 -0800
    18.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Thu Dec 04 14:43:33 2008 +0100
    18.3 @@ -485,7 +485,7 @@
    18.4                |> Syntax.check_term lthy
    18.5  
    18.6        val ((f, (_, f_defthm)), lthy) =
    18.7 -        LocalTheory.define Thm.internalK ((Name.binding (function_name fname), mixfix), ((Name.binding fdefname, []), f_def)) lthy
    18.8 +        LocalTheory.define Thm.internalK ((Binding.name (function_name fname), mixfix), ((Binding.name fdefname, []), f_def)) lthy
    18.9      in
   18.10        ((f, f_defthm), lthy)
   18.11      end
   18.12 @@ -898,7 +898,7 @@
   18.13            PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT ranT fvar f abstract_qglrs clauses RCss) lthy
   18.14  
   18.15        val (_, lthy) =
   18.16 -          LocalTheory.abbrev Syntax.mode_default ((Name.binding (dom_name defname), NoSyn), mk_acc domT R) lthy
   18.17 +          LocalTheory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
   18.18  
   18.19        val newthy = ProofContext.theory_of lthy
   18.20        val clauses = map (transfer_clause_ctx newthy) clauses
    19.1 --- a/src/HOL/Tools/function_package/fundef_lib.ML	Wed Dec 03 21:00:39 2008 -0800
    19.2 +++ b/src/HOL/Tools/function_package/fundef_lib.ML	Thu Dec 04 14:43:33 2008 +0100
    19.3 @@ -56,7 +56,7 @@
    19.4  fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
    19.5      let
    19.6        val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
    19.7 -      val (_, ctx') = ProofContext.add_fixes_i [(Name.binding n', SOME T, NoSyn)] ctx
    19.8 +      val (_, ctx') = ProofContext.add_fixes_i [(Binding.name n', SOME T, NoSyn)] ctx
    19.9  
   19.10        val (n'', body) = Term.dest_abs (n', T, b) 
   19.11        val _ = (n' = n'') orelse error "dest_all_ctx"
    20.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Dec 03 21:00:39 2008 -0800
    20.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Dec 04 14:43:33 2008 +0100
    20.3 @@ -9,14 +9,14 @@
    20.4  
    20.5  signature FUNDEF_PACKAGE =
    20.6  sig
    20.7 -    val add_fundef :  (Name.binding * string option * mixfix) list
    20.8 +    val add_fundef :  (Binding.T * string option * mixfix) list
    20.9                        -> (Attrib.binding * string) list 
   20.10                        -> FundefCommon.fundef_config
   20.11                        -> bool list
   20.12                        -> local_theory
   20.13                        -> Proof.state
   20.14  
   20.15 -    val add_fundef_i:  (Name.binding * typ option * mixfix) list
   20.16 +    val add_fundef_i:  (Binding.T * typ option * mixfix) list
   20.17                         -> (Attrib.binding * term) list
   20.18                         -> FundefCommon.fundef_config
   20.19                         -> bool list
   20.20 @@ -36,7 +36,7 @@
   20.21  open FundefLib
   20.22  open FundefCommon
   20.23  
   20.24 -fun note_theorem ((name, atts), ths) = LocalTheory.note Thm.theoremK ((Name.binding name, atts), ths)
   20.25 +fun note_theorem ((name, atts), ths) = LocalTheory.note Thm.theoremK ((Binding.name name, atts), ths)
   20.26  
   20.27  fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" 
   20.28  
   20.29 @@ -147,10 +147,10 @@
   20.30          val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
   20.31      in
   20.32        lthy
   20.33 -        |> ProofContext.note_thmss_i "" [((Name.no_binding, [ContextRules.rule_del]), [([allI], [])])] |> snd
   20.34 -        |> ProofContext.note_thmss_i "" [((Name.no_binding, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
   20.35 +        |> ProofContext.note_thmss_i "" [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
   20.36 +        |> ProofContext.note_thmss_i "" [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
   20.37          |> ProofContext.note_thmss_i ""
   20.38 -          [((Name.binding "termination", [ContextRules.intro_bang (SOME 0)]),
   20.39 +          [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
   20.40              [([Goal.norm_result termination], [])])] |> snd
   20.41          |> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]]
   20.42      end
    21.1 --- a/src/HOL/Tools/function_package/inductive_wrap.ML	Wed Dec 03 21:00:39 2008 -0800
    21.2 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Thu Dec 04 14:43:33 2008 +0100
    21.3 @@ -44,14 +44,14 @@
    21.4              {quiet_mode = false,
    21.5                verbose = ! Toplevel.debug,
    21.6                kind = Thm.internalK,
    21.7 -              alt_name = Name.no_binding,
    21.8 +              alt_name = Binding.empty,
    21.9                coind = false,
   21.10                no_elim = false,
   21.11                no_ind = false,
   21.12                skip_mono = true}
   21.13 -            [((Name.binding R, T), NoSyn)] (* the relation *)
   21.14 +            [((Binding.name R, T), NoSyn)] (* the relation *)
   21.15              [] (* no parameters *)
   21.16 -            (map (fn t => (Attrib.no_binding, t)) defs) (* the intros *)
   21.17 +            (map (fn t => (Attrib.empty_binding, t)) defs) (* the intros *)
   21.18              [] (* no special monos *)
   21.19              lthy
   21.20  
    22.1 --- a/src/HOL/Tools/function_package/mutual.ML	Wed Dec 03 21:00:39 2008 -0800
    22.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Thu Dec 04 14:43:33 2008 +0100
    22.3 @@ -150,8 +150,8 @@
    22.4        fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
    22.5            let
    22.6              val ((f, (_, f_defthm)), lthy') =
    22.7 -              LocalTheory.define Thm.internalK ((Name.binding fname, mixfix),
    22.8 -                                            ((Name.binding (fname ^ "_def"), []), Term.subst_bound (fsum, f_def)))
    22.9 +              LocalTheory.define Thm.internalK ((Binding.name fname, mixfix),
   22.10 +                                            ((Binding.name (fname ^ "_def"), []), Term.subst_bound (fsum, f_def)))
   22.11                                lthy
   22.12            in
   22.13              (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
    23.1 --- a/src/HOL/Tools/function_package/size.ML	Wed Dec 03 21:00:39 2008 -0800
    23.2 +++ b/src/HOL/Tools/function_package/size.ML	Thu Dec 04 14:43:33 2008 +0100
    23.3 @@ -89,7 +89,7 @@
    23.4        map (fn (T as Type (s, _), optname) =>
    23.5          let
    23.6            val s' = the_default (Sign.base_name s) optname ^ "_size";
    23.7 -          val s'' = Sign.full_name thy s'
    23.8 +          val s'' = Sign.full_bname thy s'
    23.9          in
   23.10            (s'',
   23.11             (list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT),
   23.12 @@ -133,7 +133,7 @@
   23.13        let
   23.14          val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
   23.15          val ((_, (_, thm)), lthy') = lthy |> LocalTheory.define Thm.definitionK
   23.16 -          ((Name.binding c, NoSyn), ((Name.binding def_name, []), rhs));
   23.17 +          ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs));
   23.18          val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy');
   23.19          val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;
   23.20        in (thm', lthy') end;
    24.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Dec 03 21:00:39 2008 -0800
    24.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Dec 04 14:43:33 2008 +0100
    24.3 @@ -1,5 +1,4 @@
    24.4  (*  Title:      HOL/Tools/inductive_package.ML
    24.5 -    ID:         $Id$
    24.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    24.7      Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
    24.8  
    24.9 @@ -39,17 +38,17 @@
   24.10      thm list list * local_theory
   24.11    type inductive_flags
   24.12    val add_inductive_i:
   24.13 -    inductive_flags -> ((Name.binding * typ) * mixfix) list ->
   24.14 +    inductive_flags -> ((Binding.T * typ) * mixfix) list ->
   24.15      (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
   24.16      inductive_result * local_theory
   24.17    val add_inductive: bool -> bool ->
   24.18 -    (Name.binding * string option * mixfix) list ->
   24.19 -    (Name.binding * string option * mixfix) list ->
   24.20 +    (Binding.T * string option * mixfix) list ->
   24.21 +    (Binding.T * string option * mixfix) list ->
   24.22      (Attrib.binding * string) list ->
   24.23      (Facts.ref * Attrib.src list) list ->
   24.24      local_theory -> inductive_result * local_theory
   24.25    val add_inductive_global: string -> inductive_flags ->
   24.26 -    ((Name.binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
   24.27 +    ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
   24.28      thm list -> theory -> inductive_result * theory
   24.29    val arities_of: thm -> (string * int) list
   24.30    val params_of: thm -> term list
   24.31 @@ -64,16 +63,16 @@
   24.32  sig
   24.33    include BASIC_INDUCTIVE_PACKAGE
   24.34    type add_ind_def
   24.35 -  val declare_rules: string -> Name.binding -> bool -> bool -> string list ->
   24.36 -    thm list -> Name.binding list -> Attrib.src list list -> (thm * string list) list ->
   24.37 +  val declare_rules: string -> Binding.T -> bool -> bool -> string list ->
   24.38 +    thm list -> Binding.T list -> Attrib.src list list -> (thm * string list) list ->
   24.39      thm -> local_theory -> thm list * thm list * thm * local_theory
   24.40    val add_ind_def: add_ind_def
   24.41    val gen_add_inductive_i: add_ind_def -> inductive_flags ->
   24.42 -    ((Name.binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
   24.43 +    ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
   24.44      thm list -> local_theory -> inductive_result * local_theory
   24.45    val gen_add_inductive: add_ind_def -> bool -> bool ->
   24.46 -    (Name.binding * string option * mixfix) list ->
   24.47 -    (Name.binding * string option * mixfix) list ->
   24.48 +    (Binding.T * string option * mixfix) list ->
   24.49 +    (Binding.T * string option * mixfix) list ->
   24.50      (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
   24.51      local_theory -> inductive_result * local_theory
   24.52    val gen_ind_decl: add_ind_def -> bool ->
   24.53 @@ -638,14 +637,14 @@
   24.54      (* add definiton of recursive predicates to theory *)
   24.55  
   24.56      val rec_name =
   24.57 -      if Binding.is_nothing alt_name then
   24.58 -        Binding.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
   24.59 +      if Binding.is_empty alt_name then
   24.60 +        Binding.name (space_implode "_" (map (Name.name_of o fst) cnames_syn))
   24.61        else alt_name;
   24.62  
   24.63      val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
   24.64        LocalTheory.define Thm.internalK
   24.65          ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
   24.66 -         (Attrib.no_binding, fold_rev lambda params
   24.67 +         (Attrib.empty_binding, fold_rev lambda params
   24.68             (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
   24.69      val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
   24.70        (cterm_of (ProofContext.theory_of ctxt') (list_comb (rec_const, params)));
   24.71 @@ -656,7 +655,7 @@
   24.72            val xs = map Free (Variable.variant_frees ctxt intr_ts
   24.73              (mk_names "x" (length Ts) ~~ Ts))
   24.74          in
   24.75 -          (name_mx, (Attrib.no_binding, fold_rev lambda (params @ xs)
   24.76 +          (name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs)
   24.77              (list_comb (rec_const, params @ make_bool_args' bs i @
   24.78                make_args argTs (xs ~~ Ts)))))
   24.79          end) (cnames_syn ~~ cs);
   24.80 @@ -673,7 +672,7 @@
   24.81        elims raw_induct ctxt =
   24.82    let
   24.83      val rec_name = Name.name_of rec_binding;
   24.84 -    val rec_qualified = Name.qualified rec_name;
   24.85 +    val rec_qualified = Binding.qualify rec_name;
   24.86      val intr_names = map Name.name_of intr_bindings;
   24.87      val ind_case_names = RuleCases.case_names intr_names;
   24.88      val induct =
   24.89 @@ -693,23 +692,23 @@
   24.90        map (hd o snd);
   24.91      val (((_, elims'), (_, [induct'])), ctxt2) =
   24.92        ctxt1 |>
   24.93 -      LocalTheory.note kind ((rec_qualified (Name.binding "intros"), []), intrs') ||>>
   24.94 +      LocalTheory.note kind ((rec_qualified (Binding.name "intros"), []), intrs') ||>>
   24.95        fold_map (fn (name, (elim, cases)) =>
   24.96 -        LocalTheory.note kind ((Name.binding (NameSpace.qualified (Sign.base_name name) "cases"),
   24.97 +        LocalTheory.note kind ((Binding.name (NameSpace.qualified (Sign.base_name name) "cases"),
   24.98            [Attrib.internal (K (RuleCases.case_names cases)),
   24.99             Attrib.internal (K (RuleCases.consumes 1)),
  24.100             Attrib.internal (K (Induct.cases_pred name)),
  24.101             Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
  24.102          apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
  24.103        LocalTheory.note kind
  24.104 -        ((rec_qualified (Name.binding (coind_prefix coind ^ "induct")),
  24.105 +        ((rec_qualified (Binding.name (coind_prefix coind ^ "induct")),
  24.106            map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]);
  24.107  
  24.108      val ctxt3 = if no_ind orelse coind then ctxt2 else
  24.109        let val inducts = cnames ~~ ProjectRule.projects ctxt2 (1 upto length cnames) induct'
  24.110        in
  24.111          ctxt2 |>
  24.112 -        LocalTheory.notes kind [((rec_qualified (Name.binding "inducts"), []),
  24.113 +        LocalTheory.notes kind [((rec_qualified (Binding.name "inducts"), []),
  24.114            inducts |> map (fn (name, th) => ([th],
  24.115              [Attrib.internal (K ind_case_names),
  24.116               Attrib.internal (K (RuleCases.consumes 1)),
  24.117 @@ -718,13 +717,13 @@
  24.118    in (intrs', elims', induct', ctxt3) end;
  24.119  
  24.120  type inductive_flags =
  24.121 -  {quiet_mode: bool, verbose: bool, kind: string, alt_name: Name.binding,
  24.122 +  {quiet_mode: bool, verbose: bool, kind: string, alt_name: Binding.T,
  24.123     coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool}
  24.124  
  24.125  type add_ind_def =
  24.126    inductive_flags ->
  24.127    term list -> (Attrib.binding * term) list -> thm list ->
  24.128 -  term list -> (Name.binding * mixfix) list ->
  24.129 +  term list -> (Binding.T * mixfix) list ->
  24.130    local_theory -> inductive_result * local_theory
  24.131  
  24.132  fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono}
  24.133 @@ -735,7 +734,7 @@
  24.134      val _ = message (quiet_mode andalso not verbose)
  24.135        ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
  24.136  
  24.137 -    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o Name.name_of o #1) cnames_syn;  (* FIXME *)
  24.138 +    val cnames = map (Sign.full_bname (ProofContext.theory_of ctxt) o Name.name_of o #1) cnames_syn;  (* FIXME *)
  24.139      val ((intr_names, intr_atts), intr_ts) =
  24.140        apfst split_list (split_list (map (check_rule ctxt cs params) intros));
  24.141  
  24.142 @@ -846,7 +845,7 @@
  24.143      val intrs = map (apsnd the_single) specs;
  24.144      val monos = Attrib.eval_thms lthy raw_monos;
  24.145      val flags = {quiet_mode = false, verbose = verbose, kind = Thm.theoremK,
  24.146 -      alt_name = Name.no_binding, coind = coind, no_elim = false, no_ind = false, skip_mono = false};
  24.147 +      alt_name = Binding.empty, coind = coind, no_elim = false, no_ind = false, skip_mono = false};
  24.148    in
  24.149      lthy
  24.150      |> LocalTheory.set_group (serial_string ())
  24.151 @@ -858,7 +857,7 @@
  24.152  
  24.153  fun add_inductive_global group flags cnames_syn pnames pre_intros monos thy =
  24.154    let
  24.155 -    val name = Sign.full_name thy (Name.name_of (fst (fst (hd cnames_syn))));
  24.156 +    val name = Sign.full_bname thy (Name.name_of (fst (fst (hd cnames_syn))));
  24.157      val ctxt' = thy
  24.158        |> TheoryTarget.init NONE
  24.159        |> LocalTheory.set_group group
    25.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Dec 03 21:00:39 2008 -0800
    25.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Dec 04 14:43:33 2008 +0100
    25.3 @@ -338,7 +338,7 @@
    25.4              (Logic.strip_assums_concl rintr));
    25.5            val s' = Sign.base_name s;
    25.6            val T' = Logic.unvarifyT T
    25.7 -        in (((Name.binding s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
    25.8 +        in (((Binding.name s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
    25.9      val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
   25.10        (List.take (snd (strip_comb
   25.11          (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
   25.12 @@ -347,10 +347,10 @@
   25.13  
   25.14      val (ind_info, thy3') = thy2 |>
   25.15        InductivePackage.add_inductive_global (serial_string ())
   25.16 -        {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Name.no_binding,
   25.17 +        {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
   25.18            coind = false, no_elim = false, no_ind = false, skip_mono = false}
   25.19          rlzpreds rlzparams (map (fn (rintr, intr) =>
   25.20 -          ((Name.binding (Sign.base_name (name_of_thm intr)), []),
   25.21 +          ((Binding.name (Sign.base_name (name_of_thm intr)), []),
   25.22             subst_atomic rlzpreds' (Logic.unvarify rintr)))
   25.23               (rintrs ~~ maps snd rss)) [] ||>
   25.24        Sign.absolute_path;
    26.1 --- a/src/HOL/Tools/inductive_set_package.ML	Wed Dec 03 21:00:39 2008 -0800
    26.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Thu Dec 04 14:43:33 2008 +0100
    26.3 @@ -1,5 +1,4 @@
    26.4  (*  Title:      HOL/Tools/inductive_set_package.ML
    26.5 -    ID:         $Id$
    26.6      Author:     Stefan Berghofer, TU Muenchen
    26.7  
    26.8  Wrapper for defining inductive sets using package for inductive predicates,
    26.9 @@ -13,13 +12,13 @@
   26.10    val pred_set_conv_att: attribute
   26.11    val add_inductive_i:
   26.12      InductivePackage.inductive_flags ->
   26.13 -    ((Name.binding * typ) * mixfix) list ->
   26.14 +    ((Binding.T * typ) * mixfix) list ->
   26.15      (string * typ) list ->
   26.16      (Attrib.binding * term) list -> thm list ->
   26.17      local_theory -> InductivePackage.inductive_result * local_theory
   26.18    val add_inductive: bool -> bool ->
   26.19 -    (Name.binding * string option * mixfix) list ->
   26.20 -    (Name.binding * string option * mixfix) list ->
   26.21 +    (Binding.T * string option * mixfix) list ->
   26.22 +    (Binding.T * string option * mixfix) list ->
   26.23      (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
   26.24      local_theory -> InductivePackage.inductive_result * local_theory
   26.25    val codegen_preproc: theory -> thm list -> thm list
   26.26 @@ -464,17 +463,17 @@
   26.27             | NONE => u)) |>
   26.28          Pattern.rewrite_term thy [] [to_pred_proc thy eqns'] |>
   26.29          eta_contract (member op = cs' orf is_pred pred_arities))) intros;
   26.30 -    val cnames_syn' = map (fn (b, _) => (Name.map_name (suffix "p") b, NoSyn)) cnames_syn;
   26.31 +    val cnames_syn' = map (fn (b, _) => (Binding.map_base (suffix "p") b, NoSyn)) cnames_syn;
   26.32      val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
   26.33      val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
   26.34        InductivePackage.add_ind_def
   26.35 -        {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Name.no_binding,
   26.36 +        {quiet_mode = quiet_mode, verbose = verbose, kind = kind, alt_name = Binding.empty,
   26.37            coind = coind, no_elim = no_elim, no_ind = no_ind, skip_mono = skip_mono}
   26.38          cs' intros' monos' params1 cnames_syn' ctxt;
   26.39  
   26.40      (* define inductive sets using previously defined predicates *)
   26.41      val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
   26.42 -      (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.no_binding,
   26.43 +      (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
   26.44           fold_rev lambda params (HOLogic.Collect_const U $
   26.45             HOLogic.ap_split' fs U HOLogic.boolT (list_comb (p, params3))))))
   26.46           (cnames_syn ~~ cs_info ~~ preds)) ctxt1;
   26.47 @@ -492,17 +491,17 @@
   26.48              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
   26.49                [def, mem_Collect_eq, split_conv]) 1))
   26.50          in
   26.51 -          ctxt |> LocalTheory.note kind ((Name.binding (s ^ "p_" ^ s ^ "_eq"),
   26.52 +          ctxt |> LocalTheory.note kind ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
   26.53              [Attrib.internal (K pred_set_conv_att)]),
   26.54                [conv_thm]) |> snd
   26.55          end) (preds ~~ cs ~~ cs_info ~~ defs) ctxt2;
   26.56  
   26.57      (* convert theorems to set notation *)
   26.58      val rec_name =
   26.59 -      if Binding.is_nothing alt_name then
   26.60 -        Binding.binding (space_implode "_" (map (Name.name_of o fst) cnames_syn))
   26.61 +      if Binding.is_empty alt_name then
   26.62 +        Binding.name (space_implode "_" (map (Name.name_of o fst) cnames_syn))
   26.63        else alt_name;
   26.64 -    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o Name.name_of o #1) cnames_syn;  (* FIXME *)
   26.65 +    val cnames = map (Sign.full_bname (ProofContext.theory_of ctxt3) o Name.name_of o #1) cnames_syn;  (* FIXME *)
   26.66      val (intr_names, intr_atts) = split_list (map fst intros);
   26.67      val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct;
   26.68      val (intrs', elims', induct, ctxt4) =
    27.1 --- a/src/HOL/Tools/primrec_package.ML	Wed Dec 03 21:00:39 2008 -0800
    27.2 +++ b/src/HOL/Tools/primrec_package.ML	Thu Dec 04 14:43:33 2008 +0100
    27.3 @@ -1,5 +1,4 @@
    27.4  (*  Title:      HOL/Tools/primrec_package.ML
    27.5 -    ID:         $Id$
    27.6      Author:     Stefan Berghofer, TU Muenchen; Norbert Voelker, FernUni Hagen;
    27.7                  Florian Haftmann, TU Muenchen
    27.8  
    27.9 @@ -8,12 +7,12 @@
   27.10  
   27.11  signature PRIMREC_PACKAGE =
   27.12  sig
   27.13 -  val add_primrec: (Name.binding * typ option * mixfix) list ->
   27.14 +  val add_primrec: (Binding.T * typ option * mixfix) list ->
   27.15      (Attrib.binding * term) list -> local_theory -> thm list * local_theory
   27.16 -  val add_primrec_global: (Name.binding * typ option * mixfix) list ->
   27.17 +  val add_primrec_global: (Binding.T * typ option * mixfix) list ->
   27.18      (Attrib.binding * term) list -> theory -> thm list * theory
   27.19    val add_primrec_overloaded: (string * (string * typ) * bool) list ->
   27.20 -    (Name.binding * typ option * mixfix) list ->
   27.21 +    (Binding.T * typ option * mixfix) list ->
   27.22      (Attrib.binding * term) list -> theory -> thm list * theory
   27.23  end;
   27.24  
   27.25 @@ -196,7 +195,7 @@
   27.26      val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
   27.27      val SOME var = get_first (fn ((b, _), mx) =>
   27.28        if Name.name_of b = fname then SOME (b, mx) else NONE) fixes;
   27.29 -  in (var, ((Name.binding def_name, []), rhs)) end;
   27.30 +  in (var, ((Binding.name def_name, []), rhs)) end;
   27.31  
   27.32  
   27.33  (* find datatypes which contain all datatypes in tnames' *)
   27.34 @@ -248,7 +247,7 @@
   27.35      val _ = if gen_eq_set (op =) (names1, names2) then ()
   27.36        else primrec_error ("functions " ^ commas_quote names2 ^
   27.37          "\nare not mutually recursive");
   27.38 -    val qualify = Name.qualified
   27.39 +    val qualify = Binding.qualify
   27.40        (space_implode "_" (map (Sign.base_name o #1) defs));
   27.41      val spec' = (map o apfst o apfst) qualify spec;
   27.42      val simp_atts = map (Attrib.internal o K)
   27.43 @@ -260,7 +259,7 @@
   27.44      |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec'))
   27.45      |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
   27.46      |-> (fn simps' => LocalTheory.note Thm.theoremK
   27.47 -          ((qualify (Name.binding "simps"), simp_atts), maps snd simps'))
   27.48 +          ((qualify (Binding.name "simps"), simp_atts), maps snd simps'))
   27.49      |>> snd
   27.50    end handle PrimrecError (msg, some_eqn) =>
   27.51      error ("Primrec definition error:\n" ^ msg ^ (case some_eqn
    28.1 --- a/src/HOL/Tools/recdef_package.ML	Wed Dec 03 21:00:39 2008 -0800
    28.2 +++ b/src/HOL/Tools/recdef_package.ML	Thu Dec 04 14:43:33 2008 +0100
    28.3 @@ -268,8 +268,8 @@
    28.4        error ("No termination condition #" ^ string_of_int i ^
    28.5          " in recdef definition of " ^ quote name);
    28.6    in
    28.7 -    Specification.theorem Thm.internalK NONE (K I) (Name.binding bname, atts)
    28.8 -      [] (Element.Shows [(Attrib.no_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
    28.9 +    Specification.theorem Thm.internalK NONE (K I) (Binding.name bname, atts)
   28.10 +      [] (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
   28.11    end;
   28.12  
   28.13  val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const;
    29.1 --- a/src/HOL/Tools/record_package.ML	Wed Dec 03 21:00:39 2008 -0800
    29.2 +++ b/src/HOL/Tools/record_package.ML	Thu Dec 04 14:43:33 2008 +0100
    29.3 @@ -1762,8 +1762,8 @@
    29.4      val external_names = NameSpace.external_names (Sign.naming_of thy);
    29.5  
    29.6      val alphas = map fst args;
    29.7 -    val name = Sign.full_name thy bname;
    29.8 -    val full = Sign.full_name_path thy bname;
    29.9 +    val name = Sign.full_bname thy bname;
   29.10 +    val full = Sign.full_bname_path thy bname;
   29.11      val base = Sign.base_name;
   29.12  
   29.13      val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
   29.14 @@ -2253,7 +2253,7 @@
   29.15  
   29.16      (* errors *)
   29.17  
   29.18 -    val name = Sign.full_name thy bname;
   29.19 +    val name = Sign.full_bname thy bname;
   29.20      val err_dup_record =
   29.21        if is_none (get_record thy name) then []
   29.22        else ["Duplicate definition of record " ^ quote name];
    30.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Dec 03 21:00:39 2008 -0800
    30.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Dec 04 14:43:33 2008 +0100
    30.3 @@ -84,10 +84,10 @@
    30.4              val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
    30.5                      (*Forms a lambda-abstraction over the formal parameters*)
    30.6              val (c, thy') =
    30.7 -              Sign.declare_const [Markup.property_internal] ((Name.binding cname, cT), NoSyn) thy
    30.8 +              Sign.declare_const [Markup.property_internal] ((Binding.name cname, cT), NoSyn) thy
    30.9              val cdef = cname ^ "_def"
   30.10              val thy'' = Theory.add_defs_i true false [(cdef, Logic.mk_equals (c, rhs))] thy'
   30.11 -            val ax = Thm.axiom thy'' (Sign.full_name thy'' cdef)
   30.12 +            val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
   30.13            in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
   30.14        | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
   30.15            (*Universal quant: insert a free variable into body and continue*)
    31.1 --- a/src/HOL/Tools/typecopy_package.ML	Wed Dec 03 21:00:39 2008 -0800
    31.2 +++ b/src/HOL/Tools/typecopy_package.ML	Thu Dec 04 14:43:33 2008 +0100
    31.3 @@ -143,7 +143,7 @@
    31.4      |> TheoryTarget.instantiation ([tyco], vs, [HOLogic.class_eq])
    31.5      |> `(fn lthy => Syntax.check_term lthy def_eq)
    31.6      |-> (fn def_eq => Specification.definition
    31.7 -         (NONE, (Attrib.no_binding, def_eq)))
    31.8 +         (NONE, (Attrib.empty_binding, def_eq)))
    31.9      |-> (fn (_, (_, def_thm)) =>
   31.10         Class.prove_instantiation_exit_result Morphism.thm
   31.11           (fn _ => fn def_thm => Class.intro_classes_tac []
    32.1 --- a/src/HOL/Tools/typedef_package.ML	Wed Dec 03 21:00:39 2008 -0800
    32.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Dec 04 14:43:33 2008 +0100
    32.3 @@ -80,7 +80,7 @@
    32.4    let
    32.5      val _ = Theory.requires thy "Typedef" "typedefs";
    32.6      val ctxt = ProofContext.init thy;
    32.7 -    val full = Sign.full_name thy;
    32.8 +    val full = Sign.full_bname thy;
    32.9  
   32.10      (*rhs*)
   32.11      val full_name = full name;
    33.1 --- a/src/HOL/Typedef.thy	Wed Dec 03 21:00:39 2008 -0800
    33.2 +++ b/src/HOL/Typedef.thy	Thu Dec 04 14:43:33 2008 +0100
    33.3 @@ -145,7 +145,7 @@
    33.4      thy
    33.5      |> TheoryTarget.instantiation ([tyco], vs, @{sort itself})
    33.6      |> `(fn lthy => Syntax.check_term lthy eq)
    33.7 -    |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
    33.8 +    |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
    33.9      |> snd
   33.10      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   33.11      |> LocalTheory.exit_global
    34.1 --- a/src/HOL/Typerep.thy	Wed Dec 03 21:00:39 2008 -0800
    34.2 +++ b/src/HOL/Typerep.thy	Thu Dec 04 14:43:33 2008 +0100
    34.3 @@ -67,7 +67,7 @@
    34.4      thy
    34.5      |> TheoryTarget.instantiation ([tyco], vs, @{sort typerep})
    34.6      |> `(fn lthy => Syntax.check_term lthy eq)
    34.7 -    |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
    34.8 +    |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
    34.9      |> snd
   34.10      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   34.11      |> LocalTheory.exit_global
    35.1 --- a/src/HOL/ex/Quickcheck.thy	Wed Dec 03 21:00:39 2008 -0800
    35.2 +++ b/src/HOL/ex/Quickcheck.thy	Thu Dec 04 14:43:33 2008 +0100
    35.3 @@ -151,11 +151,11 @@
    35.4            thy
    35.5            |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
    35.6            |> PrimrecPackage.add_primrec
    35.7 -               [(Name.binding (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)]
    35.8 -                 (map (fn eq => ((Name.no_binding, [del_func]), eq)) eqs')
    35.9 +               [(Binding.name (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)]
   35.10 +                 (map (fn eq => ((Binding.empty, [del_func]), eq)) eqs')
   35.11            |-> add_code
   35.12            |> `(fn lthy => Syntax.check_term lthy eq)
   35.13 -          |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
   35.14 +          |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
   35.15            |> snd
   35.16            |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   35.17            |> LocalTheory.exit_global
    36.1 --- a/src/HOL/ex/Term_Of_Syntax.thy	Wed Dec 03 21:00:39 2008 -0800
    36.2 +++ b/src/HOL/ex/Term_Of_Syntax.thy	Thu Dec 04 14:43:33 2008 +0100
    36.3 @@ -10,7 +10,7 @@
    36.4  begin
    36.5  
    36.6  setup {*
    36.7 -  Sign.declare_const [] ((Name.binding "rterm_of", @{typ "'a \<Rightarrow> 'b"}), NoSyn)
    36.8 +  Sign.declare_const [] ((Binding.name "rterm_of", @{typ "'a \<Rightarrow> 'b"}), NoSyn)
    36.9    #> snd
   36.10  *}
   36.11  
    37.1 --- a/src/HOLCF/Tools/domain/domain_axioms.ML	Wed Dec 03 21:00:39 2008 -0800
    37.2 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Thu Dec 04 14:43:33 2008 +0100
    37.3 @@ -120,7 +120,7 @@
    37.4  in (* local *)
    37.5  
    37.6  fun add_axioms (comp_dnam, eqs : eq list) thy' = let
    37.7 -  val comp_dname = Sign.full_name thy' comp_dnam;
    37.8 +  val comp_dname = Sign.full_bname thy' comp_dnam;
    37.9    val dnames = map (fst o fst) eqs;
   37.10    val x_name = idx_name dnames "x"; 
   37.11    fun copy_app dname = %%:(dname^"_copy")`Bound 0;
    38.1 --- a/src/HOLCF/Tools/domain/domain_extender.ML	Wed Dec 03 21:00:39 2008 -0800
    38.2 +++ b/src/HOLCF/Tools/domain/domain_extender.ML	Thu Dec 04 14:43:33 2008 +0100
    38.3 @@ -100,7 +100,7 @@
    38.4  fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
    38.5    let
    38.6      val dtnvs = map ((fn (dname,vs) => 
    38.7 -			 (Sign.full_name thy''' dname, map (Syntax.read_typ_global thy''') vs))
    38.8 +			 (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs))
    38.9                     o fst) eqs''';
   38.10      val cons''' = map snd eqs''';
   38.11      fun thy_type  (dname,tvars)  = (Sign.base_name dname, length tvars, NoSyn);
    39.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Dec 03 21:00:39 2008 -0800
    39.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Thu Dec 04 14:43:33 2008 +0100
    39.3 @@ -607,7 +607,7 @@
    39.4  
    39.5  val dnames = map (fst o fst) eqs;
    39.6  val conss  = map  snd        eqs;
    39.7 -val comp_dname = Sign.full_name thy comp_dnam;
    39.8 +val comp_dname = Sign.full_bname thy comp_dnam;
    39.9  
   39.10  val d = writeln("Proving induction properties of domain "^comp_dname^" ...");
   39.11  val pg = pg' thy;
    40.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Wed Dec 03 21:00:39 2008 -0800
    40.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Thu Dec 04 14:43:33 2008 +0100
    40.3 @@ -1,5 +1,4 @@
    40.4  (*  Title:      HOLCF/Tools/fixrec_package.ML
    40.5 -    ID:         $Id$
    40.6      Author:     Amber Telfer and Brian Huffman
    40.7  
    40.8  Recursive function definition package for HOLCF.
    40.9 @@ -10,9 +9,9 @@
   40.10    val legacy_infer_term: theory -> term -> term
   40.11    val legacy_infer_prop: theory -> term -> term
   40.12    val add_fixrec: bool -> (Attrib.binding * string) list list -> theory -> theory
   40.13 -  val add_fixrec_i: bool -> ((Name.binding * attribute list) * term) list list -> theory -> theory
   40.14 +  val add_fixrec_i: bool -> ((Binding.T * attribute list) * term) list list -> theory -> theory
   40.15    val add_fixpat: Attrib.binding * string list -> theory -> theory
   40.16 -  val add_fixpat_i: (Name.binding * attribute list) * term list -> theory -> theory
   40.17 +  val add_fixpat_i: (Binding.T * attribute list) * term list -> theory -> theory
   40.18  end;
   40.19  
   40.20  structure FixrecPackage: FIXREC_PACKAGE =
    41.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Wed Dec 03 21:00:39 2008 -0800
    41.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML	Thu Dec 04 14:43:33 2008 +0100
    41.3 @@ -54,7 +54,7 @@
    41.4  fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
    41.5    let
    41.6      val ctxt = ProofContext.init thy;
    41.7 -    val full = Sign.full_name thy;
    41.8 +    val full = Sign.full_bname thy;
    41.9  
   41.10      (*rhs*)
   41.11      val full_name = full name;
   41.12 @@ -94,7 +94,7 @@
   41.13            |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort "Porder.po"});
   41.14          val less_def' = Syntax.check_term lthy3 less_def;
   41.15          val ((_, (_, less_definition')), lthy4) = lthy3
   41.16 -          |> Specification.definition (NONE, ((Name.binding ("less_" ^ name ^ "_def"), []), less_def'));
   41.17 +          |> Specification.definition (NONE, ((Binding.name ("less_" ^ name ^ "_def"), []), less_def'));
   41.18          val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
   41.19          val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition';
   41.20          val thy5 = lthy4
    42.1 --- a/src/Pure/General/binding.ML	Wed Dec 03 21:00:39 2008 -0800
    42.2 +++ b/src/Pure/General/binding.ML	Thu Dec 04 14:43:33 2008 +0100
    42.3 @@ -15,17 +15,16 @@
    42.4  sig
    42.5    include BASIC_BINDING
    42.6    type T
    42.7 -  val binding_pos: string * Position.T -> T
    42.8 -  val binding: string -> T
    42.9 -  val no_binding: T
   42.10 -  val dest_binding: T -> (string * bool) list * string
   42.11 -  val is_nothing: T -> bool
   42.12 -  val pos_of: T -> Position.T
   42.13 - 
   42.14 -  val map_binding: ((string * bool) list * string -> (string * bool) list * string)
   42.15 -    -> T -> T
   42.16 +  val name_pos: string * Position.T -> T
   42.17 +  val name: string -> T
   42.18 +  val empty: T
   42.19 +  val map_base: (string -> string) -> T -> T
   42.20 +  val qualify: string -> T -> T
   42.21    val add_prefix: bool -> string -> T -> T
   42.22    val map_prefix: ((string * bool) list -> T -> T) -> T -> T
   42.23 +  val is_empty: T -> bool
   42.24 +  val pos_of: T -> Position.T
   42.25 +  val dest: T -> (string * bool) list * string
   42.26    val display: T -> string
   42.27  end
   42.28  
   42.29 @@ -44,22 +43,30 @@
   42.30  datatype T = Binding of ((string * bool) list * string) * Position.T;
   42.31    (* (prefix components (with mandatory flag), base name, position) *)
   42.32  
   42.33 -fun binding_pos (name, pos) = Binding (([], name), pos);
   42.34 -fun binding name = binding_pos (name, Position.none);
   42.35 -val no_binding = binding "";
   42.36 -
   42.37 -fun pos_of (Binding (_, pos)) = pos;
   42.38 -fun dest_binding (Binding (prefix_name, _)) = prefix_name;
   42.39 +fun name_pos (name, pos) = Binding (([], name), pos);
   42.40 +fun name name = name_pos (name, Position.none);
   42.41 +val empty = name "";
   42.42  
   42.43  fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos);
   42.44  
   42.45 -fun is_nothing (Binding ((_, name), _)) = name = "";
   42.46 +val map_base = map_binding o apsnd;
   42.47 +
   42.48 +fun qualify_base path name =
   42.49 +  if path = "" orelse name = "" then name
   42.50 +  else path ^ "." ^ name;
   42.51 +
   42.52 +val qualify = map_base o qualify_base;
   42.53 +  (*FIXME should all operations on bare names moved here from name_space.ML ?*)
   42.54  
   42.55  fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
   42.56    else (map_binding o apfst) (cons (prfx, sticky)) b;
   42.57  
   42.58  fun map_prefix f (Binding ((prefix, name), pos)) =
   42.59 -  f prefix (binding_pos (name, pos));
   42.60 +  f prefix (name_pos (name, pos));
   42.61 +
   42.62 +fun is_empty (Binding ((_, name), _)) = name = "";
   42.63 +fun pos_of (Binding (_, pos)) = pos;
   42.64 +fun dest (Binding (prefix_name, _)) = prefix_name;
   42.65  
   42.66  fun display (Binding ((prefix, name), _)) =
   42.67    let
    43.1 --- a/src/Pure/General/name_space.ML	Wed Dec 03 21:00:39 2008 -0800
    43.2 +++ b/src/Pure/General/name_space.ML	Thu Dec 04 14:43:33 2008 +0100
    43.3 @@ -30,27 +30,24 @@
    43.4    val get_accesses: T -> string -> xstring list
    43.5    val merge: T * T -> T
    43.6    type naming
    43.7 -  val path_of: naming -> string
    43.8 +  val default_naming: naming
    43.9 +  val declare: naming -> Binding.T -> T -> string * T
   43.10 +  val full_name: naming -> Binding.T -> string
   43.11 +  val declare_base: naming -> string -> T -> T
   43.12    val external_names: naming -> string -> string list
   43.13 -  val full: naming -> bstring -> string
   43.14 -  val declare: naming -> string -> T -> T
   43.15 -  val default_naming: naming
   43.16 +  val path_of: naming -> string
   43.17    val add_path: string -> naming -> naming
   43.18    val no_base_names: naming -> naming
   43.19    val qualified_names: naming -> naming
   43.20    val sticky_prefix: string -> naming -> naming
   43.21 -  val full_binding: naming -> Binding.T -> string
   43.22 -  val declare_binding: naming -> Binding.T -> T -> string * T
   43.23    type 'a table = T * 'a Symtab.table
   43.24    val empty_table: 'a table
   43.25 -  val table_declare: naming -> Binding.T * 'a
   43.26 +  val bind: naming -> Binding.T * 'a
   43.27      -> 'a table -> string * 'a table (*exception Symtab.DUP*)
   43.28 -  val table_declare_permissive: naming -> Binding.T * 'a
   43.29 -    -> 'a table -> string * 'a table
   43.30 -  val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
   43.31    val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
   43.32    val dest_table: 'a table -> (string * 'a) list
   43.33    val extern_table: 'a table -> (xstring * 'a) list
   43.34 +  val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
   43.35  end;
   43.36  
   43.37  structure NameSpace: NAME_SPACE =
   43.38 @@ -269,7 +266,11 @@
   43.39  
   43.40  fun full (Naming (path, (qualify, _))) = qualify path;
   43.41  
   43.42 -fun declare naming name space =
   43.43 +fun full_name naming b =
   43.44 +  let val (prefix, bname) = Binding.dest b
   43.45 +  in full (apply_prefix prefix naming) bname end;
   43.46 +
   43.47 +fun declare_base naming name space =
   43.48    if is_hidden name then
   43.49      error ("Attempt to declare hidden name " ^ quote name)
   43.50    else
   43.51 @@ -281,12 +282,12 @@
   43.52        val (accs, accs') = pairself (map implode_name) (accesses naming names);
   43.53      in space |> fold (add_name name) accs |> put_accesses name accs' end;
   43.54  
   43.55 -fun declare_binding bnaming b =
   43.56 +fun declare bnaming b =
   43.57    let
   43.58 -    val (prefix, bname) = Binding.dest_binding b;
   43.59 +    val (prefix, bname) = Binding.dest b;
   43.60      val naming = apply_prefix prefix bnaming;
   43.61      val name = full naming bname;
   43.62 -  in declare naming name #> pair name end;
   43.63 +  in declare_base naming name #> pair name end;
   43.64  
   43.65  
   43.66  
   43.67 @@ -296,21 +297,14 @@
   43.68  
   43.69  val empty_table = (empty, Symtab.empty);
   43.70  
   43.71 -fun gen_table_declare update naming (binding, x) (space, tab) =
   43.72 +fun bind naming (b, x) (space, tab) =
   43.73    let
   43.74 -    val (name, space') = declare_binding naming binding space;
   43.75 -  in (name, (space', update (name, x) tab)) end;
   43.76 -
   43.77 -fun table_declare naming = gen_table_declare Symtab.update_new naming;
   43.78 -fun table_declare_permissive naming = gen_table_declare Symtab.update naming;
   43.79 -
   43.80 -fun full_binding naming b =
   43.81 -  let val (prefix, bname) = Binding.dest_binding b
   43.82 -  in full (apply_prefix prefix naming) bname end;
   43.83 +    val (name, space') = declare naming b space;
   43.84 +  in (name, (space', Symtab.update_new (name, x) tab)) end;
   43.85  
   43.86  fun extend_table naming bentries (space, tab) =
   43.87    let val entries = map (apfst (full naming)) bentries
   43.88 -  in (fold (declare naming o #1) entries space, Symtab.extend (tab, entries)) end;
   43.89 +  in (fold (declare_base naming o #1) entries space, Symtab.extend (tab, entries)) end;
   43.90  
   43.91  fun merge_tables eq ((space1, tab1), (space2, tab2)) =
   43.92    (merge (space1, space2), Symtab.merge eq (tab1, tab2));
    44.1 --- a/src/Pure/Isar/args.ML	Wed Dec 03 21:00:39 2008 -0800
    44.2 +++ b/src/Pure/Isar/args.ML	Thu Dec 04 14:43:33 2008 +0100
    44.3 @@ -35,7 +35,7 @@
    44.4    val name_source: T list -> string * T list
    44.5    val name_source_position: T list -> (SymbolPos.text * Position.T) * T list
    44.6    val name: T list -> string * T list
    44.7 -  val binding: T list -> Name.binding * T list
    44.8 +  val binding: T list -> Binding.T * T list
    44.9    val alt_name: T list -> string * T list
   44.10    val symbol: T list -> string * T list
   44.11    val liberal_name: T list -> string * T list
   44.12 @@ -66,8 +66,8 @@
   44.13    val parse1: (string -> bool) -> OuterLex.token list -> T list * OuterLex.token list
   44.14    val attribs: (string -> string) -> T list -> src list * T list
   44.15    val opt_attribs: (string -> string) -> T list -> src list * T list
   44.16 -  val thm_name: (string -> string) -> string -> T list -> (Name.binding * src list) * T list
   44.17 -  val opt_thm_name: (string -> string) -> string -> T list -> (Name.binding * src list) * T list
   44.18 +  val thm_name: (string -> string) -> string -> T list -> (Binding.T * src list) * T list
   44.19 +  val opt_thm_name: (string -> string) -> string -> T list -> (Binding.T * src list) * T list
   44.20    val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'a * 'b
   44.21    val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
   44.22      src -> Proof.context -> 'a * Proof.context
   44.23 @@ -171,7 +171,7 @@
   44.24  val name_source_position = named >> T.source_position_of;
   44.25  
   44.26  val name = named >> T.content_of;
   44.27 -val binding = P.position name >> Binding.binding_pos;
   44.28 +val binding = P.position name >> Binding.name_pos;
   44.29  val alt_name = alt_string >> T.content_of;
   44.30  val symbol = symbolic >> T.content_of;
   44.31  val liberal_name = symbol || name;
   44.32 @@ -280,8 +280,8 @@
   44.33  
   44.34  fun opt_thm_name intern s =
   44.35    Scan.optional
   44.36 -    ((binding -- opt_attribs intern || attribs intern >> pair Name.no_binding) --| $$$ s)
   44.37 -    (Name.no_binding, []);
   44.38 +    ((binding -- opt_attribs intern || attribs intern >> pair Binding.empty) --| $$$ s)
   44.39 +    (Binding.empty, []);
   44.40  
   44.41  
   44.42  
    45.1 --- a/src/Pure/Isar/attrib.ML	Wed Dec 03 21:00:39 2008 -0800
    45.2 +++ b/src/Pure/Isar/attrib.ML	Thu Dec 04 14:43:33 2008 +0100
    45.3 @@ -1,5 +1,4 @@
    45.4  (*  Title:      Pure/Isar/attrib.ML
    45.5 -    ID:         $Id$
    45.6      Author:     Markus Wenzel, TU Muenchen
    45.7  
    45.8  Symbolic representation of attributes -- with name and syntax.
    45.9 @@ -8,8 +7,8 @@
   45.10  signature ATTRIB =
   45.11  sig
   45.12    type src = Args.src
   45.13 -  type binding = Name.binding * src list
   45.14 -  val no_binding: binding
   45.15 +  type binding = Binding.T * src list
   45.16 +  val empty_binding: binding
   45.17    val print_attributes: theory -> unit
   45.18    val intern: theory -> xstring -> string
   45.19    val intern_src: theory -> src -> src
   45.20 @@ -55,8 +54,8 @@
   45.21  
   45.22  type src = Args.src;
   45.23  
   45.24 -type binding = Name.binding * src list;
   45.25 -val no_binding: binding = (Name.no_binding, []);
   45.26 +type binding = Binding.T * src list;
   45.27 +val empty_binding: binding = (Binding.empty, []);
   45.28  
   45.29  
   45.30  
   45.31 @@ -119,7 +118,7 @@
   45.32  fun attribute thy = attribute_i thy o intern_src thy;
   45.33  
   45.34  fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
   45.35 -    [((Name.no_binding, []),
   45.36 +    [((Binding.empty, []),
   45.37        map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
   45.38    |> fst |> maps snd;
   45.39  
   45.40 @@ -373,7 +372,7 @@
   45.41  fun register_config config thy =
   45.42    let
   45.43      val bname = Config.name_of config;
   45.44 -    val name = Sign.full_name thy bname;
   45.45 +    val name = Sign.full_bname thy bname;
   45.46    in
   45.47      thy
   45.48      |> add_attributes [(bname, syntax (Scan.lift (scan_config thy config) >> Morphism.form),
    46.1 --- a/src/Pure/Isar/calculation.ML	Wed Dec 03 21:00:39 2008 -0800
    46.2 +++ b/src/Pure/Isar/calculation.ML	Thu Dec 04 14:43:33 2008 +0100
    46.3 @@ -115,7 +115,7 @@
    46.4  
    46.5  fun print_calculation false _ _ = ()
    46.6    | print_calculation true ctxt calc = Pretty.writeln
    46.7 -      (ProofContext.pretty_fact ctxt (ProofContext.full_name ctxt calculationN, calc));
    46.8 +      (ProofContext.pretty_fact ctxt (ProofContext.full_bname ctxt calculationN, calc));
    46.9  
   46.10  
   46.11  (* also and finally *)
    47.1 --- a/src/Pure/Isar/class.ML	Wed Dec 03 21:00:39 2008 -0800
    47.2 +++ b/src/Pure/Isar/class.ML	Thu Dec 04 14:43:33 2008 +0100
    47.3 @@ -96,7 +96,7 @@
    47.4      thy
    47.5      |> fold2 add_constraint (map snd consts) no_constraints
    47.6      |> prove_interpretation tac (class_name_morphism class) (Locale.Locale class)
    47.7 -          (map SOME inst, map (pair (Attrib.no_binding) o Thm.prop_of) def_facts)
    47.8 +          (map SOME inst, map (pair (Attrib.empty_binding) o Thm.prop_of) def_facts)
    47.9      ||> fold2 add_constraint (map snd consts) constraints
   47.10    end;
   47.11  
   47.12 @@ -476,7 +476,7 @@
   47.13      val inst = the_inst thy' class;
   47.14      val params = map (apsnd fst o snd) (these_params thy' [class]);
   47.15  
   47.16 -    val c' = Sign.full_name thy' c;
   47.17 +    val c' = Sign.full_bname thy' c;
   47.18      val dict' = Morphism.term phi dict;
   47.19      val dict_def = map_types Logic.unvarifyT dict';
   47.20      val ty' = Term.fastype_of dict_def;
   47.21 @@ -485,7 +485,7 @@
   47.22      fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
   47.23    in
   47.24      thy'
   47.25 -    |> Sign.declare_const pos ((Name.binding c, ty''), mx) |> snd
   47.26 +    |> Sign.declare_const pos ((Binding.name c, ty''), mx) |> snd
   47.27      |> Thm.add_def false false (c, def_eq)
   47.28      |>> Thm.symmetric
   47.29      ||>> get_axiom
   47.30 @@ -507,13 +507,13 @@
   47.31  
   47.32      val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
   47.33        (these_operations thy [class]);
   47.34 -    val c' = Sign.full_name thy' c;
   47.35 +    val c' = Sign.full_bname thy' c;
   47.36      val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
   47.37      val rhs'' = map_types Logic.varifyT rhs';
   47.38      val ty' = Term.fastype_of rhs';
   47.39    in
   47.40      thy'
   47.41 -    |> Sign.add_abbrev (#1 prmode) pos (Name.binding c, map_types Type.strip_sorts rhs'') |> snd
   47.42 +    |> Sign.add_abbrev (#1 prmode) pos (Binding.name c, map_types Type.strip_sorts rhs'') |> snd
   47.43      |> Sign.add_const_constraint (c', SOME ty')
   47.44      |> Sign.notation true prmode [(Const (c', ty'), mx)]
   47.45      |> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE))
   47.46 @@ -574,14 +574,14 @@
   47.47      val raw_params = (snd o chop (length supparams)) all_params;
   47.48      fun add_const (v, raw_ty) thy =
   47.49        let
   47.50 -        val c = Sign.full_name thy v;
   47.51 +        val c = Sign.full_bname thy v;
   47.52          val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
   47.53          val ty0 = Type.strip_sorts ty;
   47.54          val ty' = map_atyps (K (TFree (Name.aT, [class]))) ty0;
   47.55          val syn = (the_default NoSyn o AList.lookup (op =) global_syntax) v;
   47.56        in
   47.57          thy
   47.58 -        |> Sign.declare_const [] ((Name.binding v, ty0), syn)
   47.59 +        |> Sign.declare_const [] ((Binding.name v, ty0), syn)
   47.60          |> snd
   47.61          |> pair ((v, ty), (c, ty'))
   47.62        end;
   47.63 @@ -609,7 +609,7 @@
   47.64      |> add_consts bname class base_sort sups supparams global_syntax
   47.65      |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
   47.66            (map (fst o snd) params)
   47.67 -          [((Name.binding (bname ^ "_" ^ AxClass.axiomsN), []), map (globalize param_map) raw_pred)]
   47.68 +          [((Binding.name (bname ^ "_" ^ AxClass.axiomsN), []), map (globalize param_map) raw_pred)]
   47.69      #> snd
   47.70      #> `get_axiom
   47.71      #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
   47.72 @@ -618,7 +618,7 @@
   47.73  
   47.74  fun gen_class prep_spec bname raw_supclasses raw_elems thy =
   47.75    let
   47.76 -    val class = Sign.full_name thy bname;
   47.77 +    val class = Sign.full_bname thy bname;
   47.78      val (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) =
   47.79        prep_spec thy raw_supclasses raw_elems;
   47.80      val supconsts = map (apsnd fst o snd) (these_params thy sups);
    48.1 --- a/src/Pure/Isar/constdefs.ML	Wed Dec 03 21:00:39 2008 -0800
    48.2 +++ b/src/Pure/Isar/constdefs.ML	Thu Dec 04 14:43:33 2008 +0100
    48.3 @@ -1,5 +1,4 @@
    48.4  (*  Title:      Pure/Isar/constdefs.ML
    48.5 -    ID:         $Id$
    48.6      Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
    48.7  
    48.8  Old-style constant definitions, with type-inference and optional
    48.9 @@ -9,12 +8,12 @@
   48.10  
   48.11  signature CONSTDEFS =
   48.12  sig
   48.13 -  val add_constdefs: (Name.binding * string option) list *
   48.14 -    ((Name.binding * string option * mixfix) option *
   48.15 +  val add_constdefs: (Binding.T * string option) list *
   48.16 +    ((Binding.T * string option * mixfix) option *
   48.17        (Attrib.binding * string)) list -> theory -> theory
   48.18 -  val add_constdefs_i: (Name.binding * typ option) list *
   48.19 -    ((Name.binding * typ option * mixfix) option *
   48.20 -      ((Name.binding * attribute list) * term)) list -> theory -> theory
   48.21 +  val add_constdefs_i: (Binding.T * typ option) list *
   48.22 +    ((Binding.T * typ option * mixfix) option *
   48.23 +      ((Binding.T * attribute list) * term)) list -> theory -> theory
   48.24  end;
   48.25  
   48.26  structure Constdefs: CONSTDEFS =
   48.27 @@ -46,7 +45,7 @@
   48.28              err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
   48.29            else ());
   48.30  
   48.31 -    val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name thy c, T))] prop;
   48.32 +    val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
   48.33      val name = Thm.def_name_optional c (Name.name_of raw_name);
   48.34      val atts = map (prep_att thy) raw_atts;
   48.35  
    49.1 --- a/src/Pure/Isar/element.ML	Wed Dec 03 21:00:39 2008 -0800
    49.2 +++ b/src/Pure/Isar/element.ML	Thu Dec 04 14:43:33 2008 +0100
    49.3 @@ -1,5 +1,4 @@
    49.4  (*  Title:      Pure/Isar/element.ML
    49.5 -    ID:         $Id$
    49.6      Author:     Makarius
    49.7  
    49.8  Explicit data structures for some Isar language elements, with derived
    49.9 @@ -10,11 +9,11 @@
   49.10  sig
   49.11    datatype ('typ, 'term) stmt =
   49.12      Shows of (Attrib.binding * ('term * 'term list) list) list |
   49.13 -    Obtains of (Name.binding * ((Name.binding * 'typ option) list * 'term list)) list
   49.14 +    Obtains of (Binding.T * ((Binding.T * 'typ option) list * 'term list)) list
   49.15    type statement = (string, string) stmt
   49.16    type statement_i = (typ, term) stmt
   49.17    datatype ('typ, 'term, 'fact) ctxt =
   49.18 -    Fixes of (Name.binding * 'typ option * mixfix) list |
   49.19 +    Fixes of (Binding.T * 'typ option * mixfix) list |
   49.20      Constrains of (string * 'typ) list |
   49.21      Assumes of (Attrib.binding * ('term * 'term list) list) list |
   49.22      Defines of (Attrib.binding * ('term * 'term list)) list |
   49.23 @@ -24,8 +23,8 @@
   49.24    val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) ->
   49.25     (Attrib.binding * ('fact * Attrib.src list) list) list ->
   49.26     (Attrib.binding * ('c * Attrib.src list) list) list
   49.27 -  val map_ctxt: {name: Name.binding -> Name.binding,
   49.28 -    var: Name.binding * mixfix -> Name.binding * mixfix,
   49.29 +  val map_ctxt: {binding: Binding.T -> Binding.T,
   49.30 +    var: Binding.T * mixfix -> Binding.T * mixfix,
   49.31      typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
   49.32      attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
   49.33    val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
   49.34 @@ -56,7 +55,7 @@
   49.35    val rename_var_name: (string * (string * mixfix option)) list ->
   49.36      string * mixfix -> string * mixfix
   49.37    val rename_var: (string * (string * mixfix option)) list ->
   49.38 -    Name.binding * mixfix -> Name.binding * mixfix
   49.39 +    Binding.T * mixfix -> Binding.T * mixfix
   49.40    val rename_term: (string * (string * mixfix option)) list -> term -> term
   49.41    val rename_thm: (string * (string * mixfix option)) list -> thm -> thm
   49.42    val rename_morphism: (string * (string * mixfix option)) list -> morphism
   49.43 @@ -76,9 +75,9 @@
   49.44      (Attrib.binding * (thm list * Attrib.src list) list) list ->
   49.45      (Attrib.binding * (thm list * Attrib.src list) list) list
   49.46    val activate: (typ, term, Facts.ref) ctxt list -> Proof.context ->
   49.47 -    (context_i list * (Name.binding * Thm.thm list) list) * Proof.context
   49.48 +    (context_i list * (Binding.T * Thm.thm list) list) * Proof.context
   49.49    val activate_i: context_i list -> Proof.context ->
   49.50 -    (context_i list * (Name.binding * Thm.thm list) list) * Proof.context
   49.51 +    (context_i list * (Binding.T * Thm.thm list) list) * Proof.context
   49.52  end;
   49.53  
   49.54  structure Element: ELEMENT =
   49.55 @@ -90,7 +89,7 @@
   49.56  
   49.57  datatype ('typ, 'term) stmt =
   49.58    Shows of (Attrib.binding * ('term * 'term list) list) list |
   49.59 -  Obtains of (Name.binding * ((Name.binding * 'typ option) list * 'term list)) list;
   49.60 +  Obtains of (Binding.T * ((Binding.T * 'typ option) list * 'term list)) list;
   49.61  
   49.62  type statement = (string, string) stmt;
   49.63  type statement_i = (typ, term) stmt;
   49.64 @@ -99,7 +98,7 @@
   49.65  (* context *)
   49.66  
   49.67  datatype ('typ, 'term, 'fact) ctxt =
   49.68 -  Fixes of (Name.binding * 'typ option * mixfix) list |
   49.69 +  Fixes of (Binding.T * 'typ option * mixfix) list |
   49.70    Constrains of (string * 'typ) list |
   49.71    Assumes of (Attrib.binding * ('term * 'term list) list) list |
   49.72    Defines of (Attrib.binding * ('term * 'term list)) list |
   49.73 @@ -110,23 +109,23 @@
   49.74  
   49.75  fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts');
   49.76  
   49.77 -fun map_ctxt {name, var, typ, term, fact, attrib} =
   49.78 +fun map_ctxt {binding, var, typ, term, fact, attrib} =
   49.79    fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
   49.80         let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
   49.81     | Constrains xs => Constrains (xs |> map (fn (x, T) =>
   49.82 -       let val x' = Name.name_of (#1 (var (Name.binding x, NoSyn))) in (x', typ T) end))
   49.83 +       let val x' = Name.name_of (#1 (var (Binding.name x, NoSyn))) in (x', typ T) end))
   49.84     | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
   49.85 -      ((name a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps)))))
   49.86 +      ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps)))))
   49.87     | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
   49.88 -      ((name a, map attrib atts), (term t, map term ps))))
   49.89 +      ((binding a, map attrib atts), (term t, map term ps))))
   49.90     | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>
   49.91 -      ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
   49.92 +      ((binding a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
   49.93  
   49.94  fun map_ctxt_attrib attrib =
   49.95 -  map_ctxt {name = I, var = I, typ = I, term = I, fact = I, attrib = attrib};
   49.96 +  map_ctxt {binding = I, var = I, typ = I, term = I, fact = I, attrib = attrib};
   49.97  
   49.98  fun morph_ctxt phi = map_ctxt
   49.99 - {name = Morphism.name phi,
  49.100 + {binding = Morphism.binding phi,
  49.101    var = Morphism.var phi,
  49.102    typ = Morphism.typ phi,
  49.103    term = Morphism.term phi,
  49.104 @@ -138,7 +137,7 @@
  49.105  
  49.106  fun params_of (Fixes fixes) = fixes |> map
  49.107      (fn (x, SOME T, _) => (Name.name_of x, T)
  49.108 -      | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Name.display x), []))
  49.109 +      | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Binding.display x), []))
  49.110    | params_of _ = [];
  49.111  
  49.112  fun prems_of (Assumes asms) = maps (map fst o snd) asms
  49.113 @@ -163,7 +162,7 @@
  49.114  
  49.115  fun pretty_name_atts ctxt (b, atts) sep =
  49.116    let
  49.117 -    val name = Name.display b;
  49.118 +    val name = Binding.display b;
  49.119    in if name = "" andalso null atts then []
  49.120      else [Pretty.block
  49.121        (Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))]
  49.122 @@ -212,7 +211,7 @@
  49.123            Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
  49.124        | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Name.name_of x) ::
  49.125            Pretty.brk 1 :: prt_mixfix mx);
  49.126 -    fun prt_constrain (x, T) = prt_fix (Name.binding x, SOME T, NoSyn);
  49.127 +    fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
  49.128  
  49.129      fun prt_asm (a, ts) =
  49.130        Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts));
  49.131 @@ -246,13 +245,13 @@
  49.132      else Pretty.command kind
  49.133    in Pretty.block (Pretty.fbreaks (head :: prts)) end;
  49.134  
  49.135 -fun fix (x, T) = (Name.binding x, SOME T);
  49.136 +fun fix (x, T) = (Binding.name x, SOME T);
  49.137  
  49.138  fun obtain prop ctxt =
  49.139    let
  49.140      val ((xs, prop'), ctxt') = Variable.focus prop ctxt;
  49.141      val As = Logic.strip_imp_prems (Thm.term_of prop');
  49.142 -  in ((Name.no_binding, (map (fix o Term.dest_Free o Thm.term_of) xs, As)), ctxt') end;
  49.143 +  in ((Binding.empty, (map (fix o Term.dest_Free o Thm.term_of) xs, As)), ctxt') end;
  49.144  
  49.145  in
  49.146  
  49.147 @@ -275,9 +274,9 @@
  49.148      val (assumes, cases) = take_suffix (fn prem =>
  49.149        is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
  49.150    in
  49.151 -    pretty_ctxt ctxt' (Fixes (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) fixes)) @
  49.152 -    pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.no_binding, [(t, [])])) assumes)) @
  49.153 -     (if null cases then pretty_stmt ctxt' (Shows [(Attrib.no_binding, [(concl, [])])])
  49.154 +    pretty_ctxt ctxt' (Fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) fixes)) @
  49.155 +    pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.empty_binding, [(t, [])])) assumes)) @
  49.156 +     (if null cases then pretty_stmt ctxt' (Shows [(Attrib.empty_binding, [(concl, [])])])
  49.157        else
  49.158          let val (clauses, ctxt'') = fold_map (obtain o cert) cases ctxt'
  49.159          in pretty_stmt ctxt'' (Obtains clauses) end)
  49.160 @@ -398,7 +397,7 @@
  49.161    let
  49.162      val x = Name.name_of b;
  49.163      val (x', mx') = rename_var_name ren (x, mx);
  49.164 -  in (Name.binding x', mx') end;
  49.165 +  in (Binding.name x', mx') end;
  49.166  
  49.167  fun rename_term ren (Free (x, T)) = Free (rename ren x, T)
  49.168    | rename_term ren (t $ u) = rename_term ren t $ rename_term ren u
  49.169 @@ -419,7 +418,7 @@
  49.170    end;
  49.171  
  49.172  fun rename_morphism ren = Morphism.morphism
  49.173 -  {name = I, var = rename_var ren, typ = I, term = rename_term ren, fact = map (rename_thm ren)};
  49.174 +  {binding = I, var = rename_var ren, typ = I, term = rename_term ren, fact = map (rename_thm ren)};
  49.175  
  49.176  
  49.177  (* instantiate types *)
  49.178 @@ -447,7 +446,7 @@
  49.179  fun instT_morphism thy env =
  49.180    let val thy_ref = Theory.check_thy thy in
  49.181      Morphism.morphism
  49.182 -     {name = I, var = I,
  49.183 +     {binding = I, var = I,
  49.184        typ = instT_type env,
  49.185        term = instT_term env,
  49.186        fact = map (fn th => instT_thm (Theory.deref thy_ref) env th)}
  49.187 @@ -496,7 +495,7 @@
  49.188  fun inst_morphism thy envs =
  49.189    let val thy_ref = Theory.check_thy thy in
  49.190      Morphism.morphism
  49.191 -     {name = I, var = I,
  49.192 +     {binding = I, var = I,
  49.193        typ = instT_type (#1 envs),
  49.194        term = inst_term envs,
  49.195        fact = map (fn th => inst_thm (Theory.deref thy_ref) envs th)}
  49.196 @@ -528,7 +527,7 @@
  49.197      val exp_term = Drule.term_rule thy (singleton exp_fact);
  49.198      val exp_typ = Logic.type_map exp_term;
  49.199      val morphism =
  49.200 -      Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
  49.201 +      Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
  49.202    in facts_map (morph_ctxt morphism) facts end;
  49.203  
  49.204  
  49.205 @@ -553,7 +552,7 @@
  49.206          val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
  49.207          val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
  49.208              let val ((c, _), t') = LocalDefs.cert_def ctxt t
  49.209 -            in (t', ((Name.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
  49.210 +            in (t', ((Binding.map_base (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
  49.211          val (_, ctxt') =
  49.212            ctxt |> fold (Variable.auto_fixes o #1) asms
  49.213            |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
  49.214 @@ -577,7 +576,7 @@
  49.215  
  49.216  fun prep_facts prep_name get intern ctxt elem = elem |> map_ctxt
  49.217       {var = I, typ = I, term = I,
  49.218 -      name = Name.map_name prep_name,
  49.219 +      binding = Binding.map_base prep_name,
  49.220        fact = get ctxt,
  49.221        attrib = intern (ProofContext.theory_of ctxt)};
  49.222  
    50.1 --- a/src/Pure/Isar/expression.ML	Wed Dec 03 21:00:39 2008 -0800
    50.2 +++ b/src/Pure/Isar/expression.ML	Thu Dec 04 14:43:33 2008 +0100
    50.3 @@ -8,8 +8,8 @@
    50.4  sig
    50.5    datatype 'term map = Positional of 'term option list | Named of (string * 'term) list;
    50.6    type 'term expr = (string * (string * 'term map)) list;
    50.7 -  type expression = string expr * (Name.binding * string option * mixfix) list;
    50.8 -  type expression_i = term expr * (Name.binding * typ option * mixfix) list;
    50.9 +  type expression = string expr * (Binding.T * string option * mixfix) list;
   50.10 +  type expression_i = term expr * (Binding.T * typ option * mixfix) list;
   50.11  
   50.12    (* Processing of context statements *)
   50.13    val read_statement: Element.context list -> (string * string list) list list ->
   50.14 @@ -47,8 +47,8 @@
   50.15  
   50.16  type 'term expr = (string * (string * 'term map)) list;
   50.17  
   50.18 -type expression = string expr * (Name.binding * string option * mixfix) list;
   50.19 -type expression_i = term expr * (Name.binding * typ option * mixfix) list;
   50.20 +type expression = string expr * (Binding.T * string option * mixfix) list;
   50.21 +type expression_i = term expr * (Binding.T * typ option * mixfix) list;
   50.22  
   50.23  
   50.24  (** Parsing and printing **)
   50.25 @@ -164,7 +164,7 @@
   50.26                    (* FIXME: should check for bindings being the same.
   50.27                       Instead we check for equal name and syntax. *)
   50.28                    if mx1 = mx2 then mx1
   50.29 -                  else error ("Conflicting syntax for parameter" ^ quote (Name.display p) ^
   50.30 +                  else error ("Conflicting syntax for parameter" ^ quote (Binding.display p) ^
   50.31                      " in expression.")) (ps, ps')
   50.32                in (i', ps'') end) is []
   50.33            in (ps', is') end;
   50.34 @@ -228,7 +228,7 @@
   50.35      val inst = Symtab.make insts'';
   50.36    in
   50.37      (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
   50.38 -      Morphism.name_morphism (Name.qualified prfx), ctxt')
   50.39 +      Morphism.binding_morphism (Binding.qualify prfx), ctxt')
   50.40    end;
   50.41  
   50.42  
   50.43 @@ -237,7 +237,7 @@
   50.44  (** Parsing **)
   50.45  
   50.46  fun parse_elem prep_typ prep_term ctxt elem =
   50.47 -  Element.map_ctxt {name = I, var = I, typ = prep_typ ctxt,
   50.48 +  Element.map_ctxt {binding = I, var = I, typ = prep_typ ctxt,
   50.49      term = prep_term ctxt, fact = I, attrib = I} elem;
   50.50  
   50.51  fun parse_concl prep_term ctxt concl =
   50.52 @@ -316,7 +316,7 @@
   50.53        let val (vars, _) = prep_vars fixes ctxt
   50.54        in ctxt |> ProofContext.add_fixes_i vars |> snd end
   50.55    | declare_elem prep_vars (Constrains csts) ctxt =
   50.56 -      ctxt |> prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) |> snd
   50.57 +      ctxt |> prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) |> snd
   50.58    | declare_elem _ (Assumes _) ctxt = ctxt
   50.59    | declare_elem _ (Defines _) ctxt = ctxt
   50.60    | declare_elem _ (Notes _) ctxt = ctxt;
   50.61 @@ -397,10 +397,10 @@
   50.62      val defs' = map (Morphism.term morph) defs;
   50.63      val text' = text |>
   50.64        (if is_some asm
   50.65 -        then eval_text ctxt false (Assumes [(Attrib.no_binding, [(the asm', [])])])
   50.66 +        then eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])])
   50.67          else I) |>
   50.68        (if not (null defs)
   50.69 -        then eval_text ctxt false (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs'))
   50.70 +        then eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs'))
   50.71          else I)
   50.72  (* FIXME clone from new_locale.ML *)
   50.73    in ((loc, morph), text') end;
   50.74 @@ -580,7 +580,7 @@
   50.75      val exp_term = Drule.term_rule thy (singleton exp_fact);
   50.76      val exp_typ = Logic.type_map exp_term;
   50.77      val export' =
   50.78 -      Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
   50.79 +      Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
   50.80    in ((propss, deps, export'), goal_ctxt) end;
   50.81      
   50.82  in
   50.83 @@ -634,7 +634,7 @@
   50.84  
   50.85  fun def_pred bname parms defs ts norm_ts thy =
   50.86    let
   50.87 -    val name = Sign.full_name thy bname;
   50.88 +    val name = Sign.full_bname thy bname;
   50.89  
   50.90      val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
   50.91      val env = Term.add_term_free_names (body, []);
   50.92 @@ -651,7 +651,7 @@
   50.93      val ([pred_def], defs_thy) =
   50.94        thy
   50.95        |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
   50.96 -      |> Sign.declare_const [] ((Name.binding bname, predT), NoSyn) |> snd
   50.97 +      |> Sign.declare_const [] ((Binding.name bname, predT), NoSyn) |> snd
   50.98        |> PureThy.add_defs false
   50.99          [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
  50.100      val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
  50.101 @@ -693,7 +693,7 @@
  50.102              |> Sign.add_path aname
  50.103              |> Sign.no_base_names
  50.104              |> PureThy.note_thmss Thm.internalK
  50.105 -              [((Name.binding introN, []), [([intro], [NewLocale.unfold_attrib])])]
  50.106 +              [((Binding.name introN, []), [([intro], [NewLocale.unfold_attrib])])]
  50.107              ||> Sign.restore_naming thy';
  50.108            in (SOME statement, SOME intro, axioms, thy'') end;
  50.109      val (b_pred, b_intro, b_axioms, thy'''') =
  50.110 @@ -708,8 +708,8 @@
  50.111              |> Sign.add_path pname
  50.112              |> Sign.no_base_names
  50.113              |> PureThy.note_thmss Thm.internalK
  50.114 -                 [((Name.binding introN, []), [([intro], [NewLocale.intro_attrib])]),
  50.115 -                  ((Name.binding axiomsN, []),
  50.116 +                 [((Binding.name introN, []), [([intro], [NewLocale.intro_attrib])]),
  50.117 +                  ((Binding.name axiomsN, []),
  50.118                      [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
  50.119              ||> Sign.restore_naming thy''';
  50.120          in (SOME statement, SOME intro, axioms, thy'''') end;
  50.121 @@ -741,7 +741,7 @@
  50.122      bname predicate_name raw_imprt raw_body thy =
  50.123    let
  50.124      val thy_ctxt = ProofContext.init thy;
  50.125 -    val name = Sign.full_name thy bname;
  50.126 +    val name = Sign.full_bname thy bname;
  50.127      val _ = NewLocale.test_locale thy name andalso
  50.128        error ("Duplicate definition of locale " ^ quote name);
  50.129  
  50.130 @@ -765,7 +765,7 @@
  50.131        fst |> map (Element.morph_ctxt satisfy) |>
  50.132        map_filter (fn Notes notes => SOME notes | _ => NONE) |>
  50.133        (if is_some asm
  50.134 -        then cons (Thm.internalK, [((Name.binding (bname ^ "_" ^ axiomsN), []),
  50.135 +        then cons (Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []),
  50.136            [([assume (cterm_of thy' (the asm))], [(Attrib.internal o K) NewLocale.witness_attrib])])])
  50.137          else I);
  50.138  
    51.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Dec 03 21:00:39 2008 -0800
    51.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Dec 04 14:43:33 2008 +0100
    51.3 @@ -14,8 +14,8 @@
    51.4    val typed_print_translation: bool * (string * Position.T) -> theory -> theory
    51.5    val print_ast_translation: bool * (string * Position.T) -> theory -> theory
    51.6    val oracle: bstring -> SymbolPos.text * Position.T -> theory -> theory
    51.7 -  val add_axioms: ((Name.binding * string) * Attrib.src list) list -> theory -> theory
    51.8 -  val add_defs: (bool * bool) * ((Name.binding * string) * Attrib.src list) list -> theory -> theory
    51.9 +  val add_axioms: ((Binding.T * string) * Attrib.src list) list -> theory -> theory
   51.10 +  val add_defs: (bool * bool) * ((Binding.T * string) * Attrib.src list) list -> theory -> theory
   51.11    val declaration: string * Position.T -> local_theory -> local_theory
   51.12    val simproc_setup: string -> string list -> string * Position.T -> string list ->
   51.13      local_theory -> local_theory
    52.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Dec 03 21:00:39 2008 -0800
    52.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Dec 04 14:43:33 2008 +0100
    52.3 @@ -272,7 +272,7 @@
    52.4  val _ =
    52.5    OuterSyntax.local_theory "declare" "declare theorems (improper)" K.thy_decl
    52.6      (P.and_list1 SpecParse.xthms1
    52.7 -      >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.no_binding, flat args)]));
    52.8 +      >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)]));
    52.9  
   52.10  
   52.11  (* name space entry path *)
   52.12 @@ -396,7 +396,7 @@
   52.13            (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
   52.14              (Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin)));
   52.15  
   52.16 -val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Name.no_binding;
   52.17 +val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Binding.empty;
   52.18  
   52.19  val _ =
   52.20    OuterSyntax.command "sublocale"
   52.21 @@ -483,7 +483,7 @@
   52.22  fun gen_theorem kind =
   52.23    OuterSyntax.local_theory_to_proof' kind ("state " ^ kind) K.thy_goal
   52.24      (Scan.optional (SpecParse.opt_thm_name ":" --|
   52.25 -      Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) Attrib.no_binding --
   52.26 +      Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) Attrib.empty_binding --
   52.27        SpecParse.general_statement >> (fn (a, (elems, concl)) =>
   52.28          (Specification.theorem_cmd kind NONE (K I) a elems concl)));
   52.29  
    53.1 --- a/src/Pure/Isar/local_defs.ML	Wed Dec 03 21:00:39 2008 -0800
    53.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Dec 04 14:43:33 2008 +0100
    53.3 @@ -12,10 +12,10 @@
    53.4    val mk_def: Proof.context -> (string * term) list -> term list
    53.5    val expand: cterm list -> thm -> thm
    53.6    val def_export: Assumption.export
    53.7 -  val add_defs: ((Name.binding * mixfix) * ((Name.binding * attribute list) * term)) list ->
    53.8 +  val add_defs: ((Binding.T * mixfix) * ((Binding.T * attribute list) * term)) list ->
    53.9      Proof.context -> (term * (string * thm)) list * Proof.context
   53.10 -  val add_def: (Name.binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
   53.11 -  val fixed_abbrev: (Name.binding * mixfix) * term -> Proof.context ->
   53.12 +  val add_def: (Binding.T * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
   53.13 +  val fixed_abbrev: (Binding.T * mixfix) * term -> Proof.context ->
   53.14      (term * term) * Proof.context
   53.15    val export: Proof.context -> Proof.context -> thm -> thm list * thm
   53.16    val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm
   53.17 @@ -92,7 +92,7 @@
   53.18      val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
   53.19      val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
   53.20      val xs = map Name.name_of bvars;
   53.21 -    val names = map2 (Name.map_name o Thm.def_name_optional) xs bfacts;
   53.22 +    val names = map2 (Binding.map_base o Thm.def_name_optional) xs bfacts;
   53.23      val eqs = mk_def ctxt (xs ~~ rhss);
   53.24      val lhss = map (fst o Logic.dest_equals) eqs;
   53.25    in
   53.26 @@ -105,7 +105,7 @@
   53.27    end;
   53.28  
   53.29  fun add_def (var, rhs) ctxt =
   53.30 -  let val ([(lhs, (_, th))], ctxt') = add_defs [(var, ((Name.no_binding, []), rhs))] ctxt
   53.31 +  let val ([(lhs, (_, th))], ctxt') = add_defs [(var, ((Binding.empty, []), rhs))] ctxt
   53.32    in ((lhs, th), ctxt') end;
   53.33  
   53.34  
    54.1 --- a/src/Pure/Isar/local_theory.ML	Wed Dec 03 21:00:39 2008 -0800
    54.2 +++ b/src/Pure/Isar/local_theory.ML	Thu Dec 04 14:43:33 2008 +0100
    54.3 @@ -26,9 +26,9 @@
    54.4    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
    54.5    val affirm: local_theory -> local_theory
    54.6    val pretty: local_theory -> Pretty.T list
    54.7 -  val abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
    54.8 +  val abbrev: Syntax.mode -> (Binding.T * mixfix) * term -> local_theory ->
    54.9      (term * term) * local_theory
   54.10 -  val define: string -> (Name.binding * mixfix) * (Attrib.binding * term) -> local_theory ->
   54.11 +  val define: string -> (Binding.T * mixfix) * (Attrib.binding * term) -> local_theory ->
   54.12      (term * (string * thm)) * local_theory
   54.13    val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
   54.14    val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
   54.15 @@ -56,10 +56,10 @@
   54.16  
   54.17  type operations =
   54.18   {pretty: local_theory -> Pretty.T list,
   54.19 -  abbrev: Syntax.mode -> (Name.binding * mixfix) * term -> local_theory ->
   54.20 +  abbrev: Syntax.mode -> (Binding.T * mixfix) * term -> local_theory ->
   54.21      (term * term) * local_theory,
   54.22    define: string ->
   54.23 -    (Name.binding * mixfix) * (Attrib.binding * term) -> local_theory ->
   54.24 +    (Binding.T * mixfix) * (Attrib.binding * term) -> local_theory ->
   54.25      (term * (string * thm)) * local_theory,
   54.26    notes: string ->
   54.27      (Attrib.binding * (thm list * Attrib.src list) list) list ->
   54.28 @@ -142,7 +142,7 @@
   54.29    |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy))
   54.30    |> NameSpace.qualified_names;
   54.31  
   54.32 -val full_name = NameSpace.full o full_naming;
   54.33 +fun full_name naming = NameSpace.full_name (full_naming naming) o Binding.name;
   54.34  
   54.35  fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
   54.36    |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))
    55.1 --- a/src/Pure/Isar/locale.ML	Wed Dec 03 21:00:39 2008 -0800
    55.2 +++ b/src/Pure/Isar/locale.ML	Thu Dec 04 14:43:33 2008 +0100
    55.3 @@ -92,10 +92,10 @@
    55.4  
    55.5    (* Storing results *)
    55.6    val global_note_qualified: string ->
    55.7 -    ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
    55.8 +    ((Binding.T * attribute list) * (thm list * attribute list) list) list ->
    55.9      theory -> (string * thm list) list * theory
   55.10    val local_note_qualified: string ->
   55.11 -    ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
   55.12 +    ((Binding.T * attribute list) * (thm list * attribute list) list) list ->
   55.13      Proof.context -> (string * thm list) list * Proof.context
   55.14    val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
   55.15      Proof.context -> Proof.context
   55.16 @@ -104,11 +104,11 @@
   55.17    val add_declaration: string -> declaration -> Proof.context -> Proof.context
   55.18  
   55.19    (* Interpretation *)
   55.20 -  val get_interpret_morph: theory -> (Name.binding -> Name.binding) -> string * string ->
   55.21 +  val get_interpret_morph: theory -> (Binding.T -> Binding.T) -> string * string ->
   55.22      (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
   55.23      string -> term list -> Morphism.morphism
   55.24    val interpretation: (Proof.context -> Proof.context) ->
   55.25 -    (Name.binding -> Name.binding) -> expr ->
   55.26 +    (Binding.T -> Binding.T) -> expr ->
   55.27      term option list * (Attrib.binding * term) list ->
   55.28      theory ->
   55.29      (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
   55.30 @@ -117,7 +117,7 @@
   55.31    val interpretation_in_locale: (Proof.context -> Proof.context) ->
   55.32      xstring * expr -> theory -> Proof.state
   55.33    val interpret: (Proof.state -> Proof.state Seq.seq) ->
   55.34 -    (Name.binding -> Name.binding) -> expr ->
   55.35 +    (Binding.T -> Binding.T) -> expr ->
   55.36      term option list * (Attrib.binding * term) list ->
   55.37      bool -> Proof.state ->
   55.38      (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) * Proof.state
   55.39 @@ -226,7 +226,7 @@
   55.40  (** management of registrations in theories and proof contexts **)
   55.41  
   55.42  type registration =
   55.43 -  {prfx: (Name.binding -> Name.binding) * (string * string),
   55.44 +  {prfx: (Binding.T -> Binding.T) * (string * string),
   55.45        (* first component: interpretation name morphism;
   55.46           second component: parameter prefix *)
   55.47      exp: Morphism.morphism,
   55.48 @@ -248,18 +248,18 @@
   55.49      val join: T * T -> T
   55.50      val dest: theory -> T ->
   55.51        (term list *
   55.52 -        (((Name.binding -> Name.binding) * (string * string)) *
   55.53 +        (((Binding.T -> Binding.T) * (string * string)) *
   55.54           (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) *
   55.55           Element.witness list *
   55.56           thm Termtab.table)) list
   55.57      val test: theory -> T * term list -> bool
   55.58      val lookup: theory ->
   55.59        T * (term list * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
   55.60 -      (((Name.binding -> Name.binding) * (string * string)) * Element.witness list * thm Termtab.table) option
   55.61 -    val insert: theory -> term list -> ((Name.binding -> Name.binding) * (string * string)) ->
   55.62 +      (((Binding.T -> Binding.T) * (string * string)) * Element.witness list * thm Termtab.table) option
   55.63 +    val insert: theory -> term list -> ((Binding.T -> Binding.T) * (string * string)) ->
   55.64        (Morphism.morphism * ((typ Vartab.table * typ list) * (term Vartab.table * term list))) ->
   55.65        T ->
   55.66 -      T * (term list * (((Name.binding -> Name.binding) * (string * string)) * Element.witness list)) list
   55.67 +      T * (term list * (((Binding.T -> Binding.T) * (string * string)) * Element.witness list)) list
   55.68      val add_witness: term list -> Element.witness -> T -> T
   55.69      val add_equation: term list -> thm -> T -> T
   55.70  (*
   55.71 @@ -433,7 +433,8 @@
   55.72  
   55.73  fun register_locale name loc thy =
   55.74    thy |> LocalesData.map (fn (space, locs) =>
   55.75 -    (Sign.declare_name thy name space, Symtab.update (name, loc) locs));
   55.76 +    (NameSpace.declare_base (Sign.naming_of thy) name space,
   55.77 +      Symtab.update (name, loc) locs));
   55.78  
   55.79  fun change_locale name f thy =
   55.80    let
   55.81 @@ -811,7 +812,7 @@
   55.82  fun make_raw_params_elemss (params, tenv, syn) =
   55.83      [((("", map (fn p => (p, Symtab.lookup tenv p)) params), Assumed []),
   55.84        Int [Fixes (map (fn p =>
   55.85 -        (Name.binding p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
   55.86 +        (Binding.name p, Symtab.lookup tenv p, Symtab.lookup syn p |> the)) params)])];
   55.87  
   55.88  
   55.89  (* flatten_expr:
   55.90 @@ -954,7 +955,7 @@
   55.91            #> Binding.add_prefix false lprfx;
   55.92          val elem_morphism =
   55.93            Element.rename_morphism ren $>
   55.94 -          Morphism.name_morphism add_prefices $>
   55.95 +          Morphism.binding_morphism add_prefices $>
   55.96            Element.instT_morphism thy env;
   55.97          val elems' = map (Element.morph_ctxt elem_morphism) elems;
   55.98        in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
   55.99 @@ -1003,7 +1004,7 @@
  55.100          val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
  55.101          val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
  55.102              let val ((c, _), t') = LocalDefs.cert_def ctxt t
  55.103 -            in (t', ((Name.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
  55.104 +            in (t', ((Binding.map_base (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
  55.105          val (_, ctxt') =
  55.106            ctxt |> fold (Variable.auto_fixes o #1) asms
  55.107            |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
  55.108 @@ -1129,7 +1130,7 @@
  55.109        let val (vars, _) = prep_vars fixes ctxt
  55.110        in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end
  55.111    | declare_ext_elem prep_vars (Constrains csts) ctxt =
  55.112 -      let val (_, ctxt') = prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) ctxt
  55.113 +      let val (_, ctxt') = prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) ctxt
  55.114        in ([], ctxt') end
  55.115    | declare_ext_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt)
  55.116    | declare_ext_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt)
  55.117 @@ -1412,7 +1413,7 @@
  55.118        |> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt)))
  55.119    | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt
  55.120       {var = I, typ = I, term = I,
  55.121 -      name = Name.map_name prep_name,
  55.122 +      binding = Binding.map_base prep_name,
  55.123        fact = get ctxt,
  55.124        attrib = Args.assignable o intern (ProofContext.theory_of ctxt)};
  55.125  
  55.126 @@ -1637,9 +1638,9 @@
  55.127  
  55.128  fun name_morph phi_name (lprfx, pprfx) b =
  55.129    b
  55.130 -  |> (if not (Binding.is_nothing b) andalso pprfx <> ""
  55.131 +  |> (if not (Binding.is_empty b) andalso pprfx <> ""
  55.132          then Binding.add_prefix false pprfx else I)
  55.133 -  |> (if not (Binding.is_nothing b)
  55.134 +  |> (if not (Binding.is_empty b)
  55.135          then Binding.add_prefix false lprfx else I)
  55.136    |> phi_name;
  55.137  
  55.138 @@ -1651,9 +1652,9 @@
  55.139        (* FIXME sync with exp_fact *)
  55.140      val exp_typ = Logic.type_map exp_term;
  55.141      val export' =
  55.142 -      Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
  55.143 +      Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
  55.144    in
  55.145 -    Morphism.name_morphism (name_morph phi_name param_prfx) $>
  55.146 +    Morphism.binding_morphism (name_morph phi_name param_prfx) $>
  55.147        Element.inst_morphism thy insts $>
  55.148        Element.satisfy_morphism prems $>
  55.149        Morphism.term_morphism (MetaSimplifier.rewrite_term thy eqns []) $>
  55.150 @@ -1732,7 +1733,7 @@
  55.151      (fn (axiom, elems, params, decls, regs, intros, dests) =>
  55.152        (axiom, elems, params, add (decl, stamp ()) decls, regs, intros, dests))) #>
  55.153    add_thmss loc Thm.internalK
  55.154 -    [((Name.no_binding, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
  55.155 +    [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
  55.156  
  55.157  in
  55.158  
  55.159 @@ -1789,7 +1790,7 @@
  55.160  
  55.161  fun def_pred bname parms defs ts norm_ts thy =
  55.162    let
  55.163 -    val name = Sign.full_name thy bname;
  55.164 +    val name = Sign.full_bname thy bname;
  55.165  
  55.166      val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
  55.167      val env = Term.add_term_free_names (body, []);
  55.168 @@ -1806,7 +1807,7 @@
  55.169      val ([pred_def], defs_thy) =
  55.170        thy
  55.171        |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
  55.172 -      |> Sign.declare_const [] ((Name.binding bname, predT), NoSyn) |> snd
  55.173 +      |> Sign.declare_const [] ((Binding.name bname, predT), NoSyn) |> snd
  55.174        |> PureThy.add_defs false
  55.175          [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
  55.176      val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
  55.177 @@ -1876,12 +1877,12 @@
  55.178              |> def_pred aname parms defs exts exts';
  55.179            val elemss' = change_assumes_elemss axioms elemss;
  55.180            val a_elem = [(("", []),
  55.181 -            [Assumes [((Name.binding (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
  55.182 +            [Assumes [((Binding.name (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
  55.183            val (_, thy'') =
  55.184              thy'
  55.185              |> Sign.add_path aname
  55.186              |> Sign.no_base_names
  55.187 -            |> PureThy.note_thmss Thm.internalK [((Name.binding introN, []), [([intro], [])])]
  55.188 +            |> PureThy.note_thmss Thm.internalK [((Binding.name introN, []), [([intro], [])])]
  55.189              ||> Sign.restore_naming thy';
  55.190          in ((elemss', [statement]), a_elem, [intro], thy'') end;
  55.191      val (predicate, stmt', elemss'', b_intro, thy'''') =
  55.192 @@ -1894,14 +1895,14 @@
  55.193            val cstatement = Thm.cterm_of thy''' statement;
  55.194            val elemss'' = change_elemss_hyps axioms elemss';
  55.195            val b_elem = [(("", []),
  55.196 -               [Assumes [((Name.binding (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
  55.197 +               [Assumes [((Binding.name (pname ^ "_" ^ axiomsN), []), [(statement, [])])]])];
  55.198            val (_, thy'''') =
  55.199              thy'''
  55.200              |> Sign.add_path pname
  55.201              |> Sign.no_base_names
  55.202              |> PureThy.note_thmss Thm.internalK
  55.203 -                 [((Name.binding introN, []), [([intro], [])]),
  55.204 -                  ((Name.binding axiomsN, []),
  55.205 +                 [((Binding.name introN, []), [([intro], [])]),
  55.206 +                  ((Binding.name axiomsN, []),
  55.207                      [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
  55.208              ||> Sign.restore_naming thy''';
  55.209          in (([cstatement], axioms), [statement], elemss'' @ b_elem, [intro], thy'''') end;
  55.210 @@ -1918,7 +1919,7 @@
  55.211  
  55.212  fun defines_to_notes is_ext thy (Defines defs) defns =
  55.213      let
  55.214 -      val defs' = map (fn (_, (def, _)) => (Attrib.no_binding, (def, []))) defs
  55.215 +      val defs' = map (fn (_, (def, _)) => (Attrib.empty_binding, (def, []))) defs
  55.216        val notes = map (fn (a, (def, _)) =>
  55.217          (a, [([assume (cterm_of thy def)], [])])) defs
  55.218      in
  55.219 @@ -1940,7 +1941,7 @@
  55.220          "name" - locale with predicate named "name" *)
  55.221    let
  55.222      val thy_ctxt = ProofContext.init thy;
  55.223 -    val name = Sign.full_name thy bname;
  55.224 +    val name = Sign.full_bname thy bname;
  55.225      val _ = is_some (get_locale thy name) andalso
  55.226        error ("Duplicate definition of locale " ^ quote name);
  55.227  
  55.228 @@ -2007,9 +2008,9 @@
  55.229  end;
  55.230  
  55.231  val _ = Context.>> (Context.map_theory
  55.232 - (add_locale "" "var" empty [Fixes [(Name.binding (Name.internal "x"), NONE, NoSyn)]] #>
  55.233 + (add_locale "" "var" empty [Fixes [(Binding.name (Name.internal "x"), NONE, NoSyn)]] #>
  55.234    snd #> ProofContext.theory_of #>
  55.235 -  add_locale "" "struct" empty [Fixes [(Name.binding (Name.internal "S"), NONE, Structure)]] #>
  55.236 +  add_locale "" "struct" empty [Fixes [(Binding.name (Name.internal "S"), NONE, Structure)]] #>
  55.237    snd #> ProofContext.theory_of));
  55.238  
  55.239  
  55.240 @@ -2378,7 +2379,7 @@
  55.241              fun activate_elem (loc, ps) (Notes (kind, facts)) thy =
  55.242                  let
  55.243                    val att_morphism =
  55.244 -                    Morphism.name_morphism (name_morph phi_name param_prfx) $>
  55.245 +                    Morphism.binding_morphism (name_morph phi_name param_prfx) $>
  55.246                      Morphism.thm_morphism satisfy $>
  55.247                      Element.inst_morphism thy insts $>
  55.248                      Morphism.thm_morphism disch;
  55.249 @@ -2438,13 +2439,13 @@
  55.250    in
  55.251      state
  55.252      |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
  55.253 -      "interpret" NONE after_qed' (map (pair (Name.no_binding, [])) (prep_propp propss))
  55.254 +      "interpret" NONE after_qed' (map (pair (Binding.empty, [])) (prep_propp propss))
  55.255      |> Element.refine_witness |> Seq.hd
  55.256      |> pair morphs
  55.257    end;
  55.258  
  55.259  fun standard_name_morph interp_prfx b =
  55.260 -  if Binding.is_nothing b then b
  55.261 +  if Binding.is_empty b then b
  55.262    else Binding.map_prefix (fn ((lprfx, _) :: pprfx) =>
  55.263      fold (Binding.add_prefix false o fst) pprfx
  55.264      #> interp_prfx <> "" ? Binding.add_prefix true interp_prfx
    56.1 --- a/src/Pure/Isar/new_locale.ML	Wed Dec 03 21:00:39 2008 -0800
    56.2 +++ b/src/Pure/Isar/new_locale.ML	Thu Dec 04 14:43:33 2008 +0100
    56.3 @@ -11,7 +11,7 @@
    56.4    val clear_idents: Proof.context -> Proof.context
    56.5    val test_locale: theory -> string -> bool
    56.6    val register_locale: string ->
    56.7 -    (string * sort) list * (Name.binding * typ option * mixfix) list ->
    56.8 +    (string * sort) list * (Binding.T * typ option * mixfix) list ->
    56.9      term option * term list ->
   56.10      (declaration * stamp) list * (declaration * stamp) list ->
   56.11      ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list ->
   56.12 @@ -22,7 +22,7 @@
   56.13    val extern: theory -> string -> xstring
   56.14  
   56.15    (* Specification *)
   56.16 -  val params_of: theory -> string -> (Name.binding * typ option * mixfix) list
   56.17 +  val params_of: theory -> string -> (Binding.T * typ option * mixfix) list
   56.18    val specification_of: theory -> string -> term option * term list
   56.19    val declarations_of: theory -> string -> declaration list * declaration list
   56.20  
   56.21 @@ -84,7 +84,7 @@
   56.22  
   56.23  datatype locale = Loc of {
   56.24    (* extensible lists are in reverse order: decls, notes, dependencies *)
   56.25 -  parameters: (string * sort) list * (Name.binding * typ option * mixfix) list,
   56.26 +  parameters: (string * sort) list * (Binding.T * typ option * mixfix) list,
   56.27      (* type and term parameters *)
   56.28    spec: term option * term list,
   56.29      (* assumptions (as a single predicate expression) and defines *)
   56.30 @@ -138,7 +138,7 @@
   56.31  
   56.32  fun register_locale name parameters spec decls notes dependencies thy =
   56.33    thy |> LocalesData.map (fn (space, locs) =>
   56.34 -    (Sign.declare_name thy name space, Symtab.update (name,
   56.35 +    (NameSpace.declare_base (Sign.naming_of thy) name space, Symtab.update (name,
   56.36        Loc {parameters = parameters, spec = spec, decls = decls, notes = notes,
   56.37          dependencies = dependencies}) locs));
   56.38  
   56.39 @@ -279,9 +279,9 @@
   56.40      input |>
   56.41        (if not (null params) then activ_elem (Fixes params) else I) |>
   56.42        (* FIXME type parameters *)
   56.43 -      (if is_some asm then activ_elem (Assumes [(Attrib.no_binding, [(the asm, [])])]) else I) |>
   56.44 +      (if is_some asm then activ_elem (Assumes [(Attrib.empty_binding, [(the asm, [])])]) else I) |>
   56.45        (if not (null defs)
   56.46 -        then activ_elem (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs))
   56.47 +        then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
   56.48          else I) |>
   56.49        pair marked |> roundup thy (activate_notes activ_elem) (name, Morphism.identity)
   56.50    end;
   56.51 @@ -366,7 +366,7 @@
   56.52      (fn (parameters, spec, decls, notes, dependencies) =>
   56.53        (parameters, spec, add (decl, stamp ()) decls, notes, dependencies))) #>
   56.54    add_thmss loc Thm.internalK
   56.55 -    [((Name.no_binding, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
   56.56 +    [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
   56.57  
   56.58  in
   56.59  
    57.1 --- a/src/Pure/Isar/object_logic.ML	Wed Dec 03 21:00:39 2008 -0800
    57.2 +++ b/src/Pure/Isar/object_logic.ML	Thu Dec 04 14:43:33 2008 +0100
    57.3 @@ -89,7 +89,7 @@
    57.4  fun typedecl (raw_name, vs, mx) thy =
    57.5    let
    57.6      val base_sort = get_base_sort thy;
    57.7 -    val name = Sign.full_name thy (Syntax.type_name raw_name mx);
    57.8 +    val name = Sign.full_bname thy (Syntax.type_name raw_name mx);
    57.9      val _ = has_duplicates (op =) vs andalso
   57.10        error ("Duplicate parameters in type declaration: " ^ quote name);
   57.11      val n = length vs;
   57.12 @@ -107,7 +107,7 @@
   57.13  local
   57.14  
   57.15  fun gen_add_judgment add_consts (bname, T, mx) thy =
   57.16 -  let val c = Sign.full_name thy (Syntax.const_name bname mx) in
   57.17 +  let val c = Sign.full_bname thy (Syntax.const_name bname mx) in
   57.18      thy
   57.19      |> add_consts [(bname, T, mx)]
   57.20      |> (fn thy' => Theory.add_deps c (c, Sign.the_const_type thy' c) [] thy')
    58.1 --- a/src/Pure/Isar/obtain.ML	Wed Dec 03 21:00:39 2008 -0800
    58.2 +++ b/src/Pure/Isar/obtain.ML	Thu Dec 04 14:43:33 2008 +0100
    58.3 @@ -40,16 +40,16 @@
    58.4  signature OBTAIN =
    58.5  sig
    58.6    val thatN: string
    58.7 -  val obtain: string -> (Name.binding * string option * mixfix) list ->
    58.8 +  val obtain: string -> (Binding.T * string option * mixfix) list ->
    58.9      (Attrib.binding * (string * string list) list) list ->
   58.10      bool -> Proof.state -> Proof.state
   58.11 -  val obtain_i: string -> (Name.binding * typ option * mixfix) list ->
   58.12 -    ((Name.binding * attribute list) * (term * term list) list) list ->
   58.13 +  val obtain_i: string -> (Binding.T * typ option * mixfix) list ->
   58.14 +    ((Binding.T * attribute list) * (term * term list) list) list ->
   58.15      bool -> Proof.state -> Proof.state
   58.16    val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
   58.17      (cterm list * thm list) * Proof.context
   58.18 -  val guess: (Name.binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
   58.19 -  val guess_i: (Name.binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
   58.20 +  val guess: (Binding.T * string option * mixfix) list -> bool -> Proof.state -> Proof.state
   58.21 +  val guess_i: (Binding.T * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
   58.22  end;
   58.23  
   58.24  structure Obtain: OBTAIN =
   58.25 @@ -156,14 +156,14 @@
   58.26    in
   58.27      state
   58.28      |> Proof.enter_forward
   58.29 -    |> Proof.have_i NONE (K Seq.single) [((Name.no_binding, []), [(obtain_prop, [])])] int
   58.30 +    |> Proof.have_i NONE (K Seq.single) [((Binding.empty, []), [(obtain_prop, [])])] int
   58.31      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
   58.32 -    |> Proof.fix_i [(Name.binding thesisN, NONE, NoSyn)]
   58.33 +    |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
   58.34      |> Proof.assume_i
   58.35 -      [((Name.binding that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
   58.36 +      [((Binding.name that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
   58.37      |> `Proof.the_facts
   58.38      ||> Proof.chain_facts chain_facts
   58.39 -    ||> Proof.show_i NONE after_qed [((Name.no_binding, []), [(thesis, [])])] false
   58.40 +    ||> Proof.show_i NONE after_qed [((Binding.empty, []), [(thesis, [])])] false
   58.41      |-> Proof.refine_insert
   58.42    end;
   58.43  
   58.44 @@ -294,9 +294,9 @@
   58.45        in
   58.46          state'
   58.47          |> Proof.map_context (K ctxt')
   58.48 -        |> Proof.fix_i (map (fn ((x, T), mx) => (Name.binding x, SOME T, mx)) parms)
   58.49 +        |> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
   58.50          |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
   58.51 -          (obtain_export fix_ctxt rule (map cert ts)) [((Name.no_binding, []), asms)])
   58.52 +          (obtain_export fix_ctxt rule (map cert ts)) [((Binding.empty, []), asms)])
   58.53          |> Proof.add_binds_i AutoBind.no_facts
   58.54        end;
   58.55  
   58.56 @@ -311,10 +311,10 @@
   58.57      state
   58.58      |> Proof.enter_forward
   58.59      |> Proof.begin_block
   58.60 -    |> Proof.fix_i [(Name.binding AutoBind.thesisN, NONE, NoSyn)]
   58.61 +    |> Proof.fix_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)]
   58.62      |> Proof.chain_facts chain_facts
   58.63      |> Proof.local_goal print_result (K I) (apsnd (rpair I))
   58.64 -      "guess" before_qed after_qed [((Name.no_binding, []), [Logic.mk_term goal, goal])]
   58.65 +      "guess" before_qed after_qed [((Binding.empty, []), [Logic.mk_term goal, goal])]
   58.66      |> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd
   58.67    end;
   58.68  
    59.1 --- a/src/Pure/Isar/outer_parse.ML	Wed Dec 03 21:00:39 2008 -0800
    59.2 +++ b/src/Pure/Isar/outer_parse.ML	Thu Dec 04 14:43:33 2008 +0100
    59.3 @@ -61,12 +61,12 @@
    59.4    val list: (token list -> 'a * token list) -> token list -> 'a list * token list
    59.5    val list1: (token list -> 'a * token list) -> token list -> 'a list * token list
    59.6    val name: token list -> bstring * token list
    59.7 -  val binding: token list -> Name.binding * token list
    59.8 +  val binding: token list -> Binding.T * token list
    59.9    val xname: token list -> xstring * token list
   59.10    val text: token list -> string * token list
   59.11    val path: token list -> Path.T * token list
   59.12    val parname: token list -> string * token list
   59.13 -  val parbinding: token list -> Name.binding * token list
   59.14 +  val parbinding: token list -> Binding.T * token list
   59.15    val sort: token list -> string * token list
   59.16    val arity: token list -> (string * string list * string) * token list
   59.17    val multi_arity: token list -> (string list * string list * string) * token list
   59.18 @@ -81,11 +81,11 @@
   59.19    val opt_mixfix': token list -> mixfix * token list
   59.20    val where_: token list -> string * token list
   59.21    val const: token list -> (string * string * mixfix) * token list
   59.22 -  val params: token list -> (Name.binding * string option) list * token list
   59.23 -  val simple_fixes: token list -> (Name.binding * string option) list * token list
   59.24 -  val fixes: token list -> (Name.binding * string option * mixfix) list * token list
   59.25 -  val for_fixes: token list -> (Name.binding * string option * mixfix) list * token list
   59.26 -  val for_simple_fixes: token list -> (Name.binding * string option) list * token list
   59.27 +  val params: token list -> (Binding.T * string option) list * token list
   59.28 +  val simple_fixes: token list -> (Binding.T * string option) list * token list
   59.29 +  val fixes: token list -> (Binding.T * string option * mixfix) list * token list
   59.30 +  val for_fixes: token list -> (Binding.T * string option * mixfix) list * token list
   59.31 +  val for_simple_fixes: token list -> (Binding.T * string option) list * token list
   59.32    val ML_source: token list -> (SymbolPos.text * Position.T) * token list
   59.33    val doc_source: token list -> (SymbolPos.text * Position.T) * token list
   59.34    val properties: token list -> Properties.T * token list
   59.35 @@ -228,13 +228,13 @@
   59.36  (* names and text *)
   59.37  
   59.38  val name = group "name declaration" (short_ident || sym_ident || string || number);
   59.39 -val binding = position name >> Binding.binding_pos;
   59.40 +val binding = position name >> Binding.name_pos;
   59.41  val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
   59.42  val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
   59.43  val path = group "file name/path specification" name >> Path.explode;
   59.44  
   59.45  val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
   59.46 -val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Name.no_binding;
   59.47 +val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;
   59.48  
   59.49  
   59.50  (* sorts and arities *)
    60.1 --- a/src/Pure/Isar/proof.ML	Wed Dec 03 21:00:39 2008 -0800
    60.2 +++ b/src/Pure/Isar/proof.ML	Thu Dec 04 14:43:33 2008 +0100
    60.3 @@ -45,27 +45,27 @@
    60.4    val match_bind_i: (term list * term) list -> state -> state
    60.5    val let_bind: (string list * string) list -> state -> state
    60.6    val let_bind_i: (term list * term) list -> state -> state
    60.7 -  val fix: (Name.binding * string option * mixfix) list -> state -> state
    60.8 -  val fix_i: (Name.binding * typ option * mixfix) list -> state -> state
    60.9 +  val fix: (Binding.T * string option * mixfix) list -> state -> state
   60.10 +  val fix_i: (Binding.T * typ option * mixfix) list -> state -> state
   60.11    val assm: Assumption.export ->
   60.12      (Attrib.binding * (string * string list) list) list -> state -> state
   60.13    val assm_i: Assumption.export ->
   60.14 -    ((Name.binding * attribute list) * (term * term list) list) list -> state -> state
   60.15 +    ((Binding.T * attribute list) * (term * term list) list) list -> state -> state
   60.16    val assume: (Attrib.binding * (string * string list) list) list -> state -> state
   60.17 -  val assume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
   60.18 +  val assume_i: ((Binding.T * attribute list) * (term * term list) list) list ->
   60.19      state -> state
   60.20    val presume: (Attrib.binding * (string * string list) list) list -> state -> state
   60.21 -  val presume_i: ((Name.binding * attribute list) * (term * term list) list) list ->
   60.22 +  val presume_i: ((Binding.T * attribute list) * (term * term list) list) list ->
   60.23      state -> state
   60.24 -  val def: (Attrib.binding * ((Name.binding * mixfix) * (string * string list))) list ->
   60.25 +  val def: (Attrib.binding * ((Binding.T * mixfix) * (string * string list))) list ->
   60.26      state -> state
   60.27 -  val def_i: ((Name.binding * attribute list) *
   60.28 -    ((Name.binding * mixfix) * (term * term list))) list -> state -> state
   60.29 +  val def_i: ((Binding.T * attribute list) *
   60.30 +    ((Binding.T * mixfix) * (term * term list))) list -> state -> state
   60.31    val chain: state -> state
   60.32    val chain_facts: thm list -> state -> state
   60.33    val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
   60.34    val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
   60.35 -  val note_thmss_i: ((Name.binding * attribute list) *
   60.36 +  val note_thmss_i: ((Binding.T * attribute list) *
   60.37      (thm list * attribute list) list) list -> state -> state
   60.38    val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
   60.39    val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
   60.40 @@ -89,7 +89,7 @@
   60.41      (theory -> 'a -> attribute) ->
   60.42      (context * 'b list -> context * (term list list * (context -> context))) ->
   60.43      string -> Method.text option -> (thm list list -> state -> state Seq.seq) ->
   60.44 -    ((Name.binding * 'a list) * 'b) list -> state -> state
   60.45 +    ((Binding.T * 'a list) * 'b) list -> state -> state
   60.46    val local_qed: Method.text option * bool -> state -> state Seq.seq
   60.47    val theorem: Method.text option -> (thm list list -> context -> context) ->
   60.48      (string * string list) list list -> context -> state
   60.49 @@ -109,11 +109,11 @@
   60.50    val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   60.51      (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   60.52    val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   60.53 -    ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
   60.54 +    ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
   60.55    val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   60.56      (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   60.57    val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   60.58 -    ((Name.binding * attribute list) * (term * term list) list) list -> bool -> state -> state
   60.59 +    ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
   60.60    val is_relevant: state -> bool
   60.61    val future_proof: (state -> context) -> state -> context
   60.62  end;
   60.63 @@ -617,7 +617,7 @@
   60.64  
   60.65  (* note etc. *)
   60.66  
   60.67 -fun no_binding args = map (pair (Name.no_binding, [])) args;
   60.68 +fun no_binding args = map (pair (Binding.empty, [])) args;
   60.69  
   60.70  local
   60.71  
   60.72 @@ -645,7 +645,7 @@
   60.73  val local_results =
   60.74    gen_thmss (ProofContext.note_thmss_i "") (K []) I I (K I) o map (apsnd Thm.simple_fact);
   60.75  
   60.76 -fun get_thmss state srcs = the_facts (note_thmss [((Name.no_binding, []), srcs)] state);
   60.77 +fun get_thmss state srcs = the_facts (note_thmss [((Binding.empty, []), srcs)] state);
   60.78  
   60.79  end;
   60.80  
   60.81 @@ -689,14 +689,14 @@
   60.82      val atts = map (prep_att (theory_of state)) raw_atts;
   60.83      val (asms, state') = state |> map_context_result (fn ctxt =>
   60.84        ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs));
   60.85 -    val assumptions = asms |> map (fn (a, ts) => ((Name.binding a, atts), map (rpair []) ts));
   60.86 +    val assumptions = asms |> map (fn (a, ts) => ((Binding.name a, atts), map (rpair []) ts));
   60.87    in
   60.88      state'
   60.89      |> map_context (ProofContext.qualified_names #> ProofContext.no_base_names)
   60.90      |> assume_i assumptions
   60.91      |> add_binds_i AutoBind.no_facts
   60.92      |> map_context (ProofContext.restore_naming (context_of state))
   60.93 -    |> `the_facts |-> (fn thms => note_thmss_i [((Name.binding name, []), [(thms, [])])])
   60.94 +    |> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
   60.95    end;
   60.96  
   60.97  in
   60.98 @@ -1002,7 +1002,7 @@
   60.99      val statement' = (kind, [[], [Thm.term_of cprop_protected]], cprop_protected);
  60.100      val goal' = Thm.adjust_maxidx_thm ~1 (Drule.protectI RS Goal.init cprop_protected);
  60.101      fun after_qed' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [Goal.conclude th]);
  60.102 -    val this_name = ProofContext.full_name (ProofContext.reset_naming goal_ctxt) AutoBind.thisN;
  60.103 +    val this_name = ProofContext.full_bname (ProofContext.reset_naming goal_ctxt) AutoBind.thisN;
  60.104  
  60.105      fun make_result () = state
  60.106        |> map_contexts (Variable.auto_fixes prop)
    61.1 --- a/src/Pure/Isar/proof_context.ML	Wed Dec 03 21:00:39 2008 -0800
    61.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Dec 04 14:43:33 2008 +0100
    61.3 @@ -23,8 +23,8 @@
    61.4    val abbrev_mode: Proof.context -> bool
    61.5    val set_stmt: bool -> Proof.context -> Proof.context
    61.6    val naming_of: Proof.context -> NameSpace.naming
    61.7 -  val full_name: Proof.context -> bstring -> string
    61.8 -  val full_binding: Proof.context -> Name.binding -> string
    61.9 +  val full_name: Proof.context -> Binding.T -> string
   61.10 +  val full_bname: Proof.context -> bstring -> string
   61.11    val consts_of: Proof.context -> Consts.T
   61.12    val const_syntax_name: Proof.context -> string -> string
   61.13    val the_const_constraint: Proof.context -> string -> typ
   61.14 @@ -105,27 +105,27 @@
   61.15    val restore_naming: Proof.context -> Proof.context -> Proof.context
   61.16    val reset_naming: Proof.context -> Proof.context
   61.17    val note_thmss: string ->
   61.18 -    ((Name.binding * attribute list) * (Facts.ref * attribute list) list) list ->
   61.19 +    ((Binding.T * attribute list) * (Facts.ref * attribute list) list) list ->
   61.20        Proof.context -> (string * thm list) list * Proof.context
   61.21    val note_thmss_i: string ->
   61.22 -    ((Name.binding * attribute list) * (thm list * attribute list) list) list ->
   61.23 +    ((Binding.T * attribute list) * (thm list * attribute list) list) list ->
   61.24        Proof.context -> (string * thm list) list * Proof.context
   61.25    val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
   61.26 -  val read_vars: (Name.binding * string option * mixfix) list -> Proof.context ->
   61.27 -    (Name.binding * typ option * mixfix) list * Proof.context
   61.28 -  val cert_vars: (Name.binding * typ option * mixfix) list -> Proof.context ->
   61.29 -    (Name.binding * typ option * mixfix) list * Proof.context
   61.30 -  val add_fixes: (Name.binding * string option * mixfix) list ->
   61.31 +  val read_vars: (Binding.T * string option * mixfix) list -> Proof.context ->
   61.32 +    (Binding.T * typ option * mixfix) list * Proof.context
   61.33 +  val cert_vars: (Binding.T * typ option * mixfix) list -> Proof.context ->
   61.34 +    (Binding.T * typ option * mixfix) list * Proof.context
   61.35 +  val add_fixes: (Binding.T * string option * mixfix) list ->
   61.36      Proof.context -> string list * Proof.context
   61.37 -  val add_fixes_i: (Name.binding * typ option * mixfix) list ->
   61.38 +  val add_fixes_i: (Binding.T * typ option * mixfix) list ->
   61.39      Proof.context -> string list * Proof.context
   61.40    val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
   61.41    val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
   61.42    val add_assms: Assumption.export ->
   61.43 -    ((Name.binding * attribute list) * (string * string list) list) list ->
   61.44 +    ((Binding.T * attribute list) * (string * string list) list) list ->
   61.45      Proof.context -> (string * thm list) list * Proof.context
   61.46    val add_assms_i: Assumption.export ->
   61.47 -    ((Name.binding * attribute list) * (term * term list) list) list ->
   61.48 +    ((Binding.T * attribute list) * (term * term list) list) list ->
   61.49      Proof.context -> (string * thm list) list * Proof.context
   61.50    val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
   61.51    val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
   61.52 @@ -135,7 +135,7 @@
   61.53      Context.generic -> Context.generic
   61.54    val add_const_constraint: string * typ option -> Proof.context -> Proof.context
   61.55    val add_abbrev: string -> Properties.T ->
   61.56 -    Name.binding * term -> Proof.context -> (term * term) * Proof.context
   61.57 +    Binding.T * term -> Proof.context -> (term * term) * Proof.context
   61.58    val revert_abbrev: string -> string -> Proof.context -> Proof.context
   61.59    val verbose: bool ref
   61.60    val setmp_verbose: ('a -> 'b) -> 'a -> 'b
   61.61 @@ -247,8 +247,8 @@
   61.62  
   61.63  val naming_of = #naming o rep_context;
   61.64  
   61.65 -val full_name = NameSpace.full o naming_of;
   61.66 -val full_binding = NameSpace.full_binding o naming_of;
   61.67 +val full_name = NameSpace.full_name o naming_of;
   61.68 +fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name;
   61.69  
   61.70  val syntax_of = #syntax o rep_context;
   61.71  val syn_of = LocalSyntax.syn_of o syntax_of;
   61.72 @@ -965,14 +965,14 @@
   61.73  
   61.74  local
   61.75  
   61.76 -fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_binding ctxt b))
   61.77 +fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))
   61.78    | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
   61.79        (Facts.add_local do_props (naming_of ctxt) (b, ths) #> snd);
   61.80  
   61.81  fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
   61.82    let
   61.83      val pos = Binding.pos_of b;
   61.84 -    val name = full_binding ctxt b;
   61.85 +    val name = full_name ctxt b;
   61.86      val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
   61.87  
   61.88      val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts);
   61.89 @@ -991,7 +991,7 @@
   61.90  fun put_thms do_props thms ctxt = ctxt
   61.91    |> map_naming (K local_naming)
   61.92    |> ContextPosition.set_visible false
   61.93 -  |> update_thms do_props (apfst Name.binding thms)
   61.94 +  |> update_thms do_props (apfst Binding.name thms)
   61.95    |> ContextPosition.restore_visible ctxt
   61.96    |> restore_naming ctxt;
   61.97  
   61.98 @@ -1021,7 +1021,7 @@
   61.99          if internal then T
  61.100          else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
  61.101        val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;
  61.102 -      val var = (Name.map_name (K x) raw_b, opt_T, mx);
  61.103 +      val var = (Binding.map_base (K x) raw_b, opt_T, mx);
  61.104      in (var, ctxt |> declare_var (x, opt_T, mx) |> #2) end);
  61.105  
  61.106  in
  61.107 @@ -1095,7 +1095,7 @@
  61.108  fun add_abbrev mode tags (b, raw_t) ctxt =
  61.109    let
  61.110      val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
  61.111 -      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Name.display b));
  61.112 +      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.display b));
  61.113      val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
  61.114      val ((lhs, rhs), consts') = consts_of ctxt
  61.115        |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (b, t);
  61.116 @@ -1146,7 +1146,7 @@
  61.117  
  61.118  fun bind_fixes xs ctxt =
  61.119    let
  61.120 -    val (_, ctxt') = ctxt |> add_fixes_i (map (fn x => (Name.binding x, NONE, NoSyn)) xs);
  61.121 +    val (_, ctxt') = ctxt |> add_fixes_i (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
  61.122      fun bind (t as Free (x, T)) =
  61.123            if member (op =) xs x then
  61.124              (case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t)
    62.1 --- a/src/Pure/Isar/rule_insts.ML	Wed Dec 03 21:00:39 2008 -0800
    62.2 +++ b/src/Pure/Isar/rule_insts.ML	Thu Dec 04 14:43:33 2008 +0100
    62.3 @@ -284,7 +284,7 @@
    62.4          val (param_names, ctxt') = ctxt
    62.5            |> Variable.declare_thm thm
    62.6            |> Thm.fold_terms Variable.declare_constraints st
    62.7 -          |> ProofContext.add_fixes_i (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) params);
    62.8 +          |> ProofContext.add_fixes_i (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
    62.9  
   62.10          (* Process type insts: Tinsts_env *)
   62.11          fun absent xi = error
    63.1 --- a/src/Pure/Isar/spec_parse.ML	Wed Dec 03 21:00:39 2008 -0800
    63.2 +++ b/src/Pure/Isar/spec_parse.ML	Thu Dec 04 14:43:33 2008 +0100
    63.3 @@ -15,14 +15,14 @@
    63.4    val opt_thm_name: string -> token list -> Attrib.binding * token list
    63.5    val spec: token list -> (Attrib.binding * string list) * token list
    63.6    val named_spec: token list -> (Attrib.binding * string list) * token list
    63.7 -  val spec_name: token list -> ((Name.binding * string) * Attrib.src list) * token list
    63.8 -  val spec_opt_name: token list -> ((Name.binding * string) * Attrib.src list) * token list
    63.9 +  val spec_name: token list -> ((Binding.T * string) * Attrib.src list) * token list
   63.10 +  val spec_opt_name: token list -> ((Binding.T * string) * Attrib.src list) * token list
   63.11    val xthm: token list -> (Facts.ref * Attrib.src list) * token list
   63.12    val xthms1: token list -> (Facts.ref * Attrib.src list) list * token list
   63.13    val name_facts: token list ->
   63.14      (Attrib.binding * (Facts.ref * Attrib.src list) list) list * token list
   63.15    val locale_mixfix: token list -> mixfix * token list
   63.16 -  val locale_fixes: token list -> (Name.binding * string option * mixfix) list * token list
   63.17 +  val locale_fixes: token list -> (Binding.T * string option * mixfix) list * token list
   63.18    val locale_insts: token list -> (string option list * (Attrib.binding * string) list) * token list
   63.19    val class_expr: token list -> string list * token list
   63.20    val locale_expr: token list -> Locale.expr * token list
   63.21 @@ -33,8 +33,8 @@
   63.22      (Element.context list * Element.statement) * OuterLex.token list
   63.23    val statement_keyword: token list -> string * token list
   63.24    val specification: token list ->
   63.25 -    (Name.binding *
   63.26 -      ((Attrib.binding * string list) list * (Name.binding * string option) list)) list * token list
   63.27 +    (Binding.T *
   63.28 +      ((Attrib.binding * string list) list * (Binding.T * string option) list)) list * token list
   63.29  end;
   63.30  
   63.31  structure SpecParse: SPEC_PARSE =
   63.32 @@ -53,8 +53,8 @@
   63.33  fun thm_name s = P.binding -- opt_attribs --| P.$$$ s;
   63.34  
   63.35  fun opt_thm_name s =
   63.36 -  Scan.optional ((P.binding -- opt_attribs || attribs >> pair Name.no_binding) --| P.$$$ s)
   63.37 -    Attrib.no_binding;
   63.38 +  Scan.optional ((P.binding -- opt_attribs || attribs >> pair Binding.empty) --| P.$$$ s)
   63.39 +    Attrib.empty_binding;
   63.40  
   63.41  val spec = opt_thm_name ":" -- Scan.repeat1 P.prop;
   63.42  val named_spec = thm_name ":" -- Scan.repeat1 P.prop;
    64.1 --- a/src/Pure/Isar/specification.ML	Wed Dec 03 21:00:39 2008 -0800
    64.2 +++ b/src/Pure/Isar/specification.ML	Thu Dec 04 14:43:33 2008 +0100
    64.3 @@ -9,33 +9,33 @@
    64.4  signature SPECIFICATION =
    64.5  sig
    64.6    val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
    64.7 -  val check_specification: (Name.binding * typ option * mixfix) list ->
    64.8 +  val check_specification: (Binding.T * typ option * mixfix) list ->
    64.9      (Attrib.binding * term list) list list -> Proof.context ->
   64.10 -    (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   64.11 -  val read_specification: (Name.binding * string option * mixfix) list ->
   64.12 +    (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   64.13 +  val read_specification: (Binding.T * string option * mixfix) list ->
   64.14      (Attrib.binding * string list) list list -> Proof.context ->
   64.15 -    (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   64.16 -  val check_free_specification: (Name.binding * typ option * mixfix) list ->
   64.17 +    (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   64.18 +  val check_free_specification: (Binding.T * typ option * mixfix) list ->
   64.19      (Attrib.binding * term list) list -> Proof.context ->
   64.20 -    (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   64.21 -  val read_free_specification: (Name.binding * string option * mixfix) list ->
   64.22 +    (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   64.23 +  val read_free_specification: (Binding.T * string option * mixfix) list ->
   64.24      (Attrib.binding * string list) list -> Proof.context ->
   64.25 -    (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   64.26 -  val axiomatization: (Name.binding * typ option * mixfix) list ->
   64.27 +    (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   64.28 +  val axiomatization: (Binding.T * typ option * mixfix) list ->
   64.29      (Attrib.binding * term list) list -> theory ->
   64.30      (term list * (string * thm list) list) * theory
   64.31 -  val axiomatization_cmd: (Name.binding * string option * mixfix) list ->
   64.32 +  val axiomatization_cmd: (Binding.T * string option * mixfix) list ->
   64.33      (Attrib.binding * string list) list -> theory ->
   64.34      (term list * (string * thm list) list) * theory
   64.35    val definition:
   64.36 -    (Name.binding * typ option * mixfix) option * (Attrib.binding * term) ->
   64.37 +    (Binding.T * typ option * mixfix) option * (Attrib.binding * term) ->
   64.38      local_theory -> (term * (string * thm)) * local_theory
   64.39    val definition_cmd:
   64.40 -    (Name.binding * string option * mixfix) option * (Attrib.binding * string) ->
   64.41 +    (Binding.T * string option * mixfix) option * (Attrib.binding * string) ->
   64.42      local_theory -> (term * (string * thm)) * local_theory
   64.43 -  val abbreviation: Syntax.mode -> (Name.binding * typ option * mixfix) option * term ->
   64.44 +  val abbreviation: Syntax.mode -> (Binding.T * typ option * mixfix) option * term ->
   64.45      local_theory -> local_theory
   64.46 -  val abbreviation_cmd: Syntax.mode -> (Name.binding * string option * mixfix) option * string ->
   64.47 +  val abbreviation_cmd: Syntax.mode -> (Binding.T * string option * mixfix) option * string ->
   64.48      local_theory -> local_theory
   64.49    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   64.50    val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   64.51 @@ -181,10 +181,10 @@
   64.52      val (vars, [((raw_name, atts), [prop])]) =
   64.53        fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy);
   64.54      val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
   64.55 -    val name = Name.map_name (Thm.def_name_optional x) raw_name;
   64.56 +    val name = Binding.map_base (Thm.def_name_optional x) raw_name;
   64.57      val var =
   64.58        (case vars of
   64.59 -        [] => (Name.binding x, NoSyn)
   64.60 +        [] => (Binding.name x, NoSyn)
   64.61        | [((b, _), mx)] =>
   64.62            let
   64.63              val y = Name.name_of b;
   64.64 @@ -193,7 +193,7 @@
   64.65                  Position.str_of (Binding.pos_of b));
   64.66            in (b, mx) end);
   64.67      val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
   64.68 -        (var, ((Name.map_name (suffix "_raw") name, []), rhs));
   64.69 +        (var, ((Binding.map_base (suffix "_raw") name, []), rhs));
   64.70      val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
   64.71          ((name, Code.add_default_eqn_attrib :: atts), [prove lthy2 th]);
   64.72  
   64.73 @@ -217,7 +217,7 @@
   64.74      val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop));
   64.75      val var =
   64.76        (case vars of
   64.77 -        [] => (Name.binding x, NoSyn)
   64.78 +        [] => (Binding.name x, NoSyn)
   64.79        | [((b, _), mx)] =>
   64.80            let
   64.81              val y = Name.name_of b;
   64.82 @@ -312,13 +312,13 @@
   64.83          val atts = map (Attrib.internal o K)
   64.84            [RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
   64.85          val prems = subtract_prems ctxt elems_ctxt;
   64.86 -        val stmt = [((Name.no_binding, atts), [(thesis, [])])];
   64.87 +        val stmt = [((Binding.empty, atts), [(thesis, [])])];
   64.88  
   64.89          val (facts, goal_ctxt) = elems_ctxt
   64.90 -          |> (snd o ProofContext.add_fixes_i [(Name.binding AutoBind.thesisN, NONE, NoSyn)])
   64.91 +          |> (snd o ProofContext.add_fixes_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
   64.92            |> fold_map assume_case (obtains ~~ propp)
   64.93            |-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK
   64.94 -                [((Name.binding Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
   64.95 +                [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
   64.96        in ((prems, stmt, facts), goal_ctxt) end);
   64.97  
   64.98  structure TheoremHook = GenericDataFun
   64.99 @@ -348,7 +348,7 @@
  64.100          lthy
  64.101          |> LocalTheory.notes kind (map2 (fn (a, _) => fn ths => (a, [(ths, [])])) stmt results')
  64.102          |> (fn (res, lthy') =>
  64.103 -          if Binding.is_nothing name andalso null atts then
  64.104 +          if Binding.is_empty name andalso null atts then
  64.105              (ProofDisplay.print_results true lthy' ((kind, ""), res); lthy')
  64.106            else
  64.107              let
  64.108 @@ -361,7 +361,7 @@
  64.109    in
  64.110      goal_ctxt
  64.111      |> ProofContext.note_thmss_i Thm.assumptionK
  64.112 -      [((Name.binding AutoBind.assmsN, []), [(prems, [])])]
  64.113 +      [((Binding.name AutoBind.assmsN, []), [(prems, [])])]
  64.114      |> snd
  64.115      |> Proof.theorem_i before_qed after_qed' (map snd stmt)
  64.116      |> Proof.refine_insert facts
    65.1 --- a/src/Pure/Isar/theory_target.ML	Wed Dec 03 21:00:39 2008 -0800
    65.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Dec 04 14:43:33 2008 +0100
    65.3 @@ -59,9 +59,9 @@
    65.4    let
    65.5      val thy = ProofContext.theory_of ctxt;
    65.6      val target_name = (if is_class then "class " else "locale ") ^ locale_extern thy target;
    65.7 -    val fixes = map (fn (x, T) => (Name.binding x, SOME T, NoSyn))
    65.8 +    val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
    65.9        (#1 (ProofContext.inferred_fixes ctxt));
   65.10 -    val assumes = map (fn A => (Attrib.no_binding, [(Thm.term_of A, [])]))
   65.11 +    val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
   65.12        (Assumption.assms_of ctxt);
   65.13      val elems =
   65.14        (if null fixes then [] else [Element.Fixes fixes]) @
   65.15 @@ -195,13 +195,13 @@
   65.16  
   65.17  fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) tags ((b, mx), rhs) phi =
   65.18    let
   65.19 -    val b' = Morphism.name phi b;
   65.20 +    val b' = Morphism.binding phi b;
   65.21      val rhs' = Morphism.term phi rhs;
   65.22      val legacy_arg = (b', Term.close_schematic_term (Logic.legacy_varify rhs'));
   65.23      val arg = (b', Term.close_schematic_term rhs');
   65.24      val similar_body = Type.similar_types (rhs, rhs');
   65.25      (* FIXME workaround based on educated guess *)
   65.26 -    val (prefix', _) = Binding.dest_binding b';
   65.27 +    val (prefix', _) = Binding.dest b';
   65.28      val class_global = Name.name_of b = Name.name_of b'
   65.29        andalso not (null prefix')
   65.30        andalso (fst o snd o split_last) prefix' = Class.class_prefix target;
   65.31 @@ -292,7 +292,7 @@
   65.32      val thy_ctxt = ProofContext.init thy;
   65.33  
   65.34      val c = Name.name_of b;
   65.35 -    val name' = Name.map_name (Thm.def_name_optional c) name;
   65.36 +    val name' = Binding.map_base (Thm.def_name_optional c) name;
   65.37      val (rhs', rhs_conv) =
   65.38        LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
   65.39      val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
    66.1 --- a/src/Pure/ROOT.ML	Wed Dec 03 21:00:39 2008 -0800
    66.2 +++ b/src/Pure/ROOT.ML	Thu Dec 04 14:43:33 2008 +0100
    66.3 @@ -1,5 +1,4 @@
    66.4  (*  Title:      Pure/ROOT.ML
    66.5 -    ID:         $Id$
    66.6  
    66.7  Pure Isabelle.
    66.8  *)
    67.1 --- a/src/Pure/Tools/invoke.ML	Wed Dec 03 21:00:39 2008 -0800
    67.2 +++ b/src/Pure/Tools/invoke.ML	Thu Dec 04 14:43:33 2008 +0100
    67.3 @@ -1,5 +1,4 @@
    67.4  (*  Title:      Pure/Tools/invoke.ML
    67.5 -    ID:         $Id$
    67.6      Author:     Makarius
    67.7  
    67.8  Schematic invocation of locale expression in proof context.
    67.9 @@ -8,9 +7,9 @@
   67.10  signature INVOKE =
   67.11  sig
   67.12    val invoke: string * Attrib.src list -> Locale.expr -> string option list ->
   67.13 -    (Name.binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
   67.14 +    (Binding.T * string option * mixfix) list -> bool -> Proof.state -> Proof.state
   67.15    val invoke_i: string * attribute list -> Locale.expr -> term option list ->
   67.16 -    (Name.binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
   67.17 +    (Binding.T * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
   67.18  end;
   67.19  
   67.20  structure Invoke: INVOKE =
   67.21 @@ -60,9 +59,9 @@
   67.22          | NONE => Drule.termI)) params';
   67.23  
   67.24      val propp =
   67.25 -      [((Name.no_binding, []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
   67.26 -       ((Name.no_binding, []), map (rpair [] o Logic.mk_term) params'),
   67.27 -       ((Name.no_binding, []), map (rpair [] o Element.mark_witness) prems')];
   67.28 +      [((Binding.empty, []), map (rpair [] o Logic.mk_term o Logic.mk_type) types'),
   67.29 +       ((Binding.empty, []), map (rpair [] o Logic.mk_term) params'),
   67.30 +       ((Binding.empty, []), map (rpair [] o Element.mark_witness) prems')];
   67.31      fun after_qed results =
   67.32        Proof.end_block #>
   67.33        Proof.map_context (fn ctxt =>
    68.1 --- a/src/Pure/assumption.ML	Wed Dec 03 21:00:39 2008 -0800
    68.2 +++ b/src/Pure/assumption.ML	Thu Dec 04 14:43:33 2008 +0100
    68.3 @@ -120,6 +120,6 @@
    68.4      val thm = export false inner outer;
    68.5      val term = export_term inner outer;
    68.6      val typ = Logic.type_map term;
    68.7 -  in Morphism.morphism {name = I, var = I, typ = typ, term = term, fact = map thm} end;
    68.8 +  in Morphism.morphism {binding = I, var = I, typ = typ, term = term, fact = map thm} end;
    68.9  
   68.10  end;
    69.1 --- a/src/Pure/axclass.ML	Wed Dec 03 21:00:39 2008 -0800
    69.2 +++ b/src/Pure/axclass.ML	Thu Dec 04 14:43:33 2008 +0100
    69.3 @@ -9,7 +9,7 @@
    69.4  signature AX_CLASS =
    69.5  sig
    69.6    val define_class: bstring * class list -> string list ->
    69.7 -    ((Name.binding * attribute list) * term list) list -> theory -> class * theory
    69.8 +    ((Binding.T * attribute list) * term list) list -> theory -> class * theory
    69.9    val add_classrel: thm -> theory -> theory
   69.10    val add_arity: thm -> theory -> theory
   69.11    val prove_classrel: class * class -> tactic -> theory -> theory
   69.12 @@ -370,7 +370,7 @@
   69.13      thy
   69.14      |> Sign.sticky_prefix name_inst
   69.15      |> Sign.no_base_names
   69.16 -    |> Sign.declare_const [] ((Name.binding c', T'), NoSyn)
   69.17 +    |> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
   69.18      |-> (fn const' as Const (c'', _) => Thm.add_def false true
   69.19            (Thm.def_name c', Logic.mk_equals (Const (c, T'), const'))
   69.20      #>> Thm.varifyT
   69.21 @@ -422,7 +422,7 @@
   69.22      (* class *)
   69.23  
   69.24      val bconst = Logic.const_of_class bclass;
   69.25 -    val class = Sign.full_name thy bclass;
   69.26 +    val class = Sign.full_bname thy bclass;
   69.27      val super = Sign.minimize_sort thy (Sign.certify_sort thy raw_super);
   69.28  
   69.29      fun check_constraint (a, S) =
   69.30 @@ -482,9 +482,9 @@
   69.31        |> Sign.add_path bconst
   69.32        |> Sign.no_base_names
   69.33        |> PureThy.note_thmss ""
   69.34 -        [((Name.binding introN, []), [([Drule.standard raw_intro], [])]),
   69.35 -         ((Name.binding superN, []), [(map Drule.standard raw_classrel, [])]),
   69.36 -         ((Name.binding axiomsN, []),
   69.37 +        [((Binding.name introN, []), [([Drule.standard raw_intro], [])]),
   69.38 +         ((Binding.name superN, []), [(map Drule.standard raw_classrel, [])]),
   69.39 +         ((Binding.name axiomsN, []),
   69.40             [(map (fn th => Drule.standard (class_triv RS th)) raw_axioms, [])])]
   69.41        ||> Sign.restore_naming def_thy;
   69.42  
   69.43 @@ -530,7 +530,7 @@
   69.44  
   69.45  fun ax_class prep_class prep_classrel (bclass, raw_super) thy =
   69.46    let
   69.47 -    val class = Sign.full_name thy bclass;
   69.48 +    val class = Sign.full_bname thy bclass;
   69.49      val super = map (prep_class thy) raw_super |> Sign.minimize_sort thy;
   69.50    in
   69.51      thy
    70.1 --- a/src/Pure/consts.ML	Wed Dec 03 21:00:39 2008 -0800
    70.2 +++ b/src/Pure/consts.ML	Thu Dec 04 14:43:33 2008 +0100
    70.3 @@ -30,10 +30,10 @@
    70.4    val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
    70.5    val typargs: T -> string * typ -> typ list
    70.6    val instance: T -> string * typ list -> typ
    70.7 -  val declare: bool -> NameSpace.naming -> Properties.T -> (Name.binding * typ) -> T -> T
    70.8 +  val declare: bool -> NameSpace.naming -> Properties.T -> (Binding.T * typ) -> T -> T
    70.9    val constrain: string * typ option -> T -> T
   70.10    val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
   70.11 -    Name.binding * term -> T -> (term * term) * T
   70.12 +    Binding.T * term -> T -> (term * term) * T
   70.13    val revert_abbrev: string -> string -> T -> T
   70.14    val hide: bool -> string -> T -> T
   70.15    val empty: T
   70.16 @@ -211,7 +211,7 @@
   70.17  fun err_dup_const c =
   70.18    error ("Duplicate declaration of constant " ^ quote c);
   70.19  
   70.20 -fun extend_decls naming decl tab = NameSpace.table_declare naming decl tab
   70.21 +fun extend_decls naming decl tab = NameSpace.bind naming decl tab
   70.22    handle Symtab.DUP c => err_dup_const c;
   70.23  
   70.24  
   70.25 @@ -273,7 +273,7 @@
   70.26        |> cert_term;
   70.27      val normal_rhs = expand_term rhs;
   70.28      val T = Term.fastype_of rhs;
   70.29 -    val lhs = Const (NameSpace.full_binding naming b, T);
   70.30 +    val lhs = Const (NameSpace.full_name naming b, T);
   70.31  
   70.32      fun err msg = error (msg ^ " on rhs of abbreviation:\n" ^
   70.33        Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs)));
    71.1 --- a/src/Pure/facts.ML	Wed Dec 03 21:00:39 2008 -0800
    71.2 +++ b/src/Pure/facts.ML	Thu Dec 04 14:43:33 2008 +0100
    71.3 @@ -31,9 +31,9 @@
    71.4    val props: T -> thm list
    71.5    val could_unify: T -> term -> thm list
    71.6    val merge: T * T -> T
    71.7 -  val add_global: NameSpace.naming -> Name.binding * thm list -> T -> string * T
    71.8 -  val add_local: bool -> NameSpace.naming -> Name.binding * thm list -> T -> string * T
    71.9 -  val add_dynamic: NameSpace.naming -> Name.binding * (Context.generic -> thm list) -> T -> string * T
   71.10 +  val add_global: NameSpace.naming -> Binding.T * thm list -> T -> string * T
   71.11 +  val add_local: bool -> NameSpace.naming -> Binding.T * thm list -> T -> string * T
   71.12 +  val add_dynamic: NameSpace.naming -> Binding.T * (Context.generic -> thm list) -> T -> string * T
   71.13    val del: string -> T -> T
   71.14    val hide: bool -> string -> T -> T
   71.15  end;
   71.16 @@ -192,10 +192,10 @@
   71.17  
   71.18  fun add permissive do_props naming (b, ths) (Facts {facts, props}) =
   71.19    let
   71.20 -    val (name, facts') = if Binding.is_nothing b then ("", facts)
   71.21 +    val (name, facts') = if Binding.is_empty b then ("", facts)
   71.22        else let
   71.23          val (space, tab) = facts;
   71.24 -        val (name, space') = NameSpace.declare_binding naming b space;
   71.25 +        val (name, space') = NameSpace.declare naming b space;
   71.26          val entry = (name, (Static ths, serial ()));
   71.27          val tab' = (if permissive then Symtab.update else Symtab.update_new) entry tab
   71.28            handle Symtab.DUP dup => err_dup_fact dup;
   71.29 @@ -213,7 +213,7 @@
   71.30  
   71.31  fun add_dynamic naming (b, f) (Facts {facts = (space, tab), props}) =
   71.32    let
   71.33 -    val (name, space') = NameSpace.declare_binding naming b space;
   71.34 +    val (name, space') = NameSpace.declare naming b space;
   71.35      val entry = (name, (Dynamic f, serial ()));
   71.36      val tab' = Symtab.update_new entry tab
   71.37        handle Symtab.DUP dup => err_dup_fact dup;
    72.1 --- a/src/Pure/more_thm.ML	Wed Dec 03 21:00:39 2008 -0800
    72.2 +++ b/src/Pure/more_thm.ML	Thu Dec 04 14:43:33 2008 +0100
    72.3 @@ -281,7 +281,7 @@
    72.4    let
    72.5      val name' = if name = "" then "axiom_" ^ serial_string () else name;
    72.6      val thy' = thy |> Theory.add_axioms_i [(name', prop)];
    72.7 -    val axm = unvarify (Thm.axiom thy' (Sign.full_name thy' name'));
    72.8 +    val axm = unvarify (Thm.axiom thy' (Sign.full_bname thy' name'));
    72.9    in (axm, thy') end;
   72.10  
   72.11  fun add_def unchecked overloaded (name, prop) thy =
   72.12 @@ -293,7 +293,7 @@
   72.13  
   72.14      val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
   72.15      val thy' = Theory.add_defs_i unchecked overloaded [(name, prop')] thy;
   72.16 -    val axm' = Thm.axiom thy' (Sign.full_name thy' name);
   72.17 +    val axm' = Thm.axiom thy' (Sign.full_bname thy' name);
   72.18      val thm = unvarify (Thm.instantiate (recover_sorts, []) axm');
   72.19    in (thm, thy') end;
   72.20  
    73.1 --- a/src/Pure/morphism.ML	Wed Dec 03 21:00:39 2008 -0800
    73.2 +++ b/src/Pure/morphism.ML	Thu Dec 04 14:43:33 2008 +0100
    73.3 @@ -1,5 +1,4 @@
    73.4  (*  Title:      Pure/morphism.ML
    73.5 -    ID:         $Id$
    73.6      Author:     Makarius
    73.7  
    73.8  Abstract morphisms on formal entities.
    73.9 @@ -17,21 +16,21 @@
   73.10  signature MORPHISM =
   73.11  sig
   73.12    include BASIC_MORPHISM
   73.13 -  val var: morphism -> Name.binding * mixfix -> Name.binding * mixfix
   73.14 -  val name: morphism -> Name.binding -> Name.binding
   73.15 +  val var: morphism -> Binding.T * mixfix -> Binding.T * mixfix
   73.16 +  val binding: morphism -> Binding.T -> Binding.T
   73.17    val typ: morphism -> typ -> typ
   73.18    val term: morphism -> term -> term
   73.19    val fact: morphism -> thm list -> thm list
   73.20    val thm: morphism -> thm -> thm
   73.21    val cterm: morphism -> cterm -> cterm
   73.22    val morphism:
   73.23 -   {name: Name.binding -> Name.binding,
   73.24 -    var: Name.binding * mixfix -> Name.binding * mixfix,
   73.25 +   {binding: Binding.T -> Binding.T,
   73.26 +    var: Binding.T * mixfix -> Binding.T * mixfix,
   73.27      typ: typ -> typ,
   73.28      term: term -> term,
   73.29      fact: thm list -> thm list} -> morphism
   73.30 -  val name_morphism: (Name.binding -> Name.binding) -> morphism
   73.31 -  val var_morphism: (Name.binding * mixfix -> Name.binding * mixfix) -> morphism
   73.32 +  val binding_morphism: (Binding.T -> Binding.T) -> morphism
   73.33 +  val var_morphism: (Binding.T * mixfix -> Binding.T * mixfix) -> morphism
   73.34    val typ_morphism: (typ -> typ) -> morphism
   73.35    val term_morphism: (term -> term) -> morphism
   73.36    val fact_morphism: (thm list -> thm list) -> morphism
   73.37 @@ -46,15 +45,15 @@
   73.38  struct
   73.39  
   73.40  datatype morphism = Morphism of
   73.41 - {name: Name.binding -> Name.binding,
   73.42 -  var: Name.binding * mixfix -> Name.binding * mixfix,
   73.43 + {binding: Binding.T -> Binding.T,
   73.44 +  var: Binding.T * mixfix -> Binding.T * mixfix,
   73.45    typ: typ -> typ,
   73.46    term: term -> term,
   73.47    fact: thm list -> thm list};
   73.48  
   73.49  type declaration = morphism -> Context.generic -> Context.generic;
   73.50  
   73.51 -fun name (Morphism {name, ...}) = name;
   73.52 +fun binding (Morphism {binding, ...}) = binding;
   73.53  fun var (Morphism {var, ...}) = var;
   73.54  fun typ (Morphism {typ, ...}) = typ;
   73.55  fun term (Morphism {term, ...}) = term;
   73.56 @@ -64,19 +63,19 @@
   73.57  
   73.58  val morphism = Morphism;
   73.59  
   73.60 -fun name_morphism name = morphism {name = name, var = I, typ = I, term = I, fact = I};
   73.61 -fun var_morphism var = morphism {name = I, var = var, typ = I, term = I, fact = I};
   73.62 -fun typ_morphism typ = morphism {name = I, var = I, typ = typ, term = I, fact = I};
   73.63 -fun term_morphism term = morphism {name = I, var = I, typ = I, term = term, fact = I};
   73.64 -fun fact_morphism fact = morphism {name = I, var = I, typ = I, term = I, fact = fact};
   73.65 -fun thm_morphism thm = morphism {name = I, var = I, typ = I, term = I, fact = map thm};
   73.66 +fun binding_morphism binding = morphism {binding = binding, var = I, typ = I, term = I, fact = I};
   73.67 +fun var_morphism var = morphism {binding = I, var = var, typ = I, term = I, fact = I};
   73.68 +fun typ_morphism typ = morphism {binding = I, var = I, typ = typ, term = I, fact = I};
   73.69 +fun term_morphism term = morphism {binding = I, var = I, typ = I, term = term, fact = I};
   73.70 +fun fact_morphism fact = morphism {binding = I, var = I, typ = I, term = I, fact = fact};
   73.71 +fun thm_morphism thm = morphism {binding = I, var = I, typ = I, term = I, fact = map thm};
   73.72  
   73.73 -val identity = morphism {name = I, var = I, typ = I, term = I, fact = I};
   73.74 +val identity = morphism {binding = I, var = I, typ = I, term = I, fact = I};
   73.75  
   73.76  fun compose
   73.77 -    (Morphism {name = name1, var = var1, typ = typ1, term = term1, fact = fact1})
   73.78 -    (Morphism {name = name2, var = var2, typ = typ2, term = term2, fact = fact2}) =
   73.79 -  morphism {name = name1 o name2, var = var1 o var2,
   73.80 +    (Morphism {binding = binding1, var = var1, typ = typ1, term = term1, fact = fact1})
   73.81 +    (Morphism {binding = binding2, var = var2, typ = typ2, term = term2, fact = fact2}) =
   73.82 +  morphism {binding = binding1 o binding2, var = var1 o var2,
   73.83      typ = typ1 o typ2, term = term1 o term2, fact = fact1 o fact2};
   73.84  
   73.85  fun phi1 $> phi2 = compose phi2 phi1;
    74.1 --- a/src/Pure/name.ML	Wed Dec 03 21:00:39 2008 -0800
    74.2 +++ b/src/Pure/name.ML	Thu Dec 04 14:43:33 2008 +0100
    74.3 @@ -1,8 +1,7 @@
    74.4  (*  Title:      Pure/name.ML
    74.5 -    ID:         $Id$
    74.6      Author:     Makarius
    74.7  
    74.8 -Names of basic logical entities (variables etc.).  Generic name bindings.
    74.9 +Names of basic logical entities (variables etc.).
   74.10  *)
   74.11  
   74.12  signature NAME =
   74.13 @@ -29,11 +28,7 @@
   74.14    val variant_list: string list -> string list -> string list
   74.15    val variant: string list -> string -> string
   74.16  
   74.17 -  include BINDING
   74.18 -  type binding = Binding.T
   74.19    val name_of: Binding.T -> string (*FIMXE legacy*)
   74.20 -  val map_name: (string -> string) -> Binding.T -> Binding.T (*FIMXE legacy*)
   74.21 -  val qualified: string -> Binding.T -> Binding.T (*FIMXE legacy*)
   74.22  end;
   74.23  
   74.24  structure Name: NAME =
   74.25 @@ -146,15 +141,8 @@
   74.26  fun variant used = singleton (variant_list used);
   74.27  
   74.28  
   74.29 -(** generic name bindings **)
   74.30 -
   74.31 -open Binding;
   74.32 +(** generic name bindings -- legacy **)
   74.33  
   74.34 -type binding = Binding.T;
   74.35 -
   74.36 -val prefix_of = fst o dest_binding;
   74.37 -val name_of = snd o dest_binding;
   74.38 -val map_name = map_binding o apsnd;
   74.39 -val qualified = map_name o NameSpace.qualified;
   74.40 +val name_of = snd o Binding.dest;
   74.41  
   74.42  end;
    75.1 --- a/src/Pure/pure_thy.ML	Wed Dec 03 21:00:39 2008 -0800
    75.2 +++ b/src/Pure/pure_thy.ML	Thu Dec 04 14:43:33 2008 +0100
    75.3 @@ -31,9 +31,9 @@
    75.4    val add_thm: (bstring * thm) * attribute list -> theory -> thm * theory
    75.5    val add_thmss: ((bstring * thm list) * attribute list) list -> theory -> thm list list * theory
    75.6    val add_thms_dynamic: bstring * (Context.generic -> thm list) -> theory -> theory
    75.7 -  val note_thmss: string -> ((Name.binding * attribute list) *
    75.8 +  val note_thmss: string -> ((Binding.T * attribute list) *
    75.9      (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
   75.10 -  val note_thmss_grouped: string -> string -> ((Name.binding * attribute list) *
   75.11 +  val note_thmss_grouped: string -> string -> ((Binding.T * attribute list) *
   75.12      (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
   75.13    val add_axioms: ((bstring * term) * attribute list) list -> theory -> thm list * theory
   75.14    val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory
   75.15 @@ -144,11 +144,11 @@
   75.16    (FactsData.map (apsnd (fold (cons o lazy_proof) thms)) thy, thms);
   75.17  
   75.18  fun enter_thms pre_name post_name app_att (b, thms) thy =
   75.19 -  if Binding.is_nothing b
   75.20 +  if Binding.is_empty b
   75.21    then swap (enter_proofs (app_att (thy, thms)))
   75.22    else let
   75.23      val naming = Sign.naming_of thy;
   75.24 -    val name = NameSpace.full_binding naming b;
   75.25 +    val name = NameSpace.full_name naming b;
   75.26      val (thy', thms') =
   75.27        enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
   75.28      val thms'' = map (Thm.transfer thy') thms';
   75.29 @@ -159,20 +159,20 @@
   75.30  (* store_thm(s) *)
   75.31  
   75.32  fun store_thms (bname, thms) = enter_thms (name_thms true true Position.none)
   75.33 -  (name_thms false true Position.none) I (Name.binding bname, thms);
   75.34 +  (name_thms false true Position.none) I (Binding.name bname, thms);
   75.35  
   75.36  fun store_thm (bname, th) = store_thms (bname, [th]) #>> the_single;
   75.37  
   75.38  fun store_thm_open (bname, th) =
   75.39    enter_thms (name_thms true false Position.none) (name_thms false false Position.none) I
   75.40 -    (Name.binding bname, [th]) #>> the_single;
   75.41 +    (Binding.name bname, [th]) #>> the_single;
   75.42  
   75.43  
   75.44  (* add_thms(s) *)
   75.45  
   75.46  fun add_thms_atts pre_name ((bname, thms), atts) =
   75.47    enter_thms pre_name (name_thms false true Position.none)
   75.48 -    (foldl_map (Thm.theory_attributes atts)) (Name.binding bname, thms);
   75.49 +    (foldl_map (Thm.theory_attributes atts)) (Binding.name bname, thms);
   75.50  
   75.51  fun gen_add_thmss pre_name =
   75.52    fold_map (add_thms_atts pre_name);
   75.53 @@ -189,7 +189,7 @@
   75.54  
   75.55  fun add_thms_dynamic (bname, f) thy = thy
   75.56    |> (FactsData.map o apfst)
   75.57 -      (Facts.add_dynamic (Sign.naming_of thy) (Name.binding bname, f) #> snd);
   75.58 +      (Facts.add_dynamic (Sign.naming_of thy) (Binding.name bname, f) #> snd);
   75.59  
   75.60  
   75.61  (* note_thmss *)
   75.62 @@ -199,7 +199,7 @@
   75.63  fun gen_note_thmss tag = fold_map (fn ((b, more_atts), ths_atts) => fn thy =>
   75.64    let
   75.65      val pos = Binding.pos_of b;
   75.66 -    val name = Sign.full_binding thy b;
   75.67 +    val name = Sign.full_name thy b;
   75.68      val _ = Position.report (Markup.fact_decl name) pos;
   75.69  
   75.70      fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths);
   75.71 @@ -219,7 +219,7 @@
   75.72  (* store axioms as theorems *)
   75.73  
   75.74  local
   75.75 -  fun get_ax thy (name, _) = Thm.axiom thy (Sign.full_name thy name);
   75.76 +  fun get_ax thy (name, _) = Thm.axiom thy (Sign.full_bname thy name);
   75.77    fun get_axs thy named_axs = map (Thm.forall_elim_vars 0 o get_ax thy) named_axs;
   75.78    fun add_axm add = fold_map (fn ((name, ax), atts) => fn thy =>
   75.79      let
    76.1 --- a/src/Pure/sign.ML	Wed Dec 03 21:00:39 2008 -0800
    76.2 +++ b/src/Pure/sign.ML	Thu Dec 04 14:43:33 2008 +0100
    76.3 @@ -14,11 +14,10 @@
    76.4      tsig: Type.tsig,
    76.5      consts: Consts.T}
    76.6    val naming_of: theory -> NameSpace.naming
    76.7 +  val full_name: theory -> Binding.T -> string
    76.8    val base_name: string -> bstring
    76.9 -  val full_name: theory -> bstring -> string
   76.10 -  val full_binding: theory -> Name.binding -> string
   76.11 -  val full_name_path: theory -> string -> bstring -> string
   76.12 -  val declare_name: theory -> string -> NameSpace.T -> NameSpace.T
   76.13 +  val full_bname: theory -> bstring -> string
   76.14 +  val full_bname_path: theory -> string -> bstring -> string
   76.15    val syn_of: theory -> Syntax.syntax
   76.16    val tsig_of: theory -> Type.tsig
   76.17    val classes_of: theory -> Sorts.algebra
   76.18 @@ -92,10 +91,10 @@
   76.19    val del_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
   76.20    val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
   76.21    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
   76.22 -  val declare_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
   76.23 +  val declare_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory
   76.24    val add_consts: (bstring * string * mixfix) list -> theory -> theory
   76.25    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
   76.26 -  val add_abbrev: string -> Properties.T -> Name.binding * term -> theory -> (term * term) * theory
   76.27 +  val add_abbrev: string -> Properties.T -> Binding.T * term -> theory -> (term * term) * theory
   76.28    val revert_abbrev: string -> string -> theory -> theory
   76.29    val add_const_constraint: string * typ option -> theory -> theory
   76.30    val primitive_class: string * class list -> theory -> theory
   76.31 @@ -189,10 +188,10 @@
   76.32  val naming_of = #naming o rep_sg;
   76.33  val base_name = NameSpace.base;
   76.34  
   76.35 -val full_name = NameSpace.full o naming_of;
   76.36 -val full_binding = NameSpace.full_binding o naming_of;
   76.37 -fun full_name_path thy elems = NameSpace.full (NameSpace.add_path elems (naming_of thy));
   76.38 -val declare_name = NameSpace.declare o naming_of;
   76.39 +val full_name = NameSpace.full_name o naming_of;
   76.40 +fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name;
   76.41 +fun full_bname_path thy elems =
   76.42 +  NameSpace.full_name (NameSpace.add_path elems (naming_of thy)) o Binding.name;
   76.43  
   76.44  
   76.45  (* syntax *)
   76.46 @@ -510,11 +509,11 @@
   76.47      fun prep (raw_b, raw_T, raw_mx) =
   76.48        let
   76.49          val (mx_name, mx) = Syntax.const_mixfix (Name.name_of raw_b) raw_mx;
   76.50 -        val b = Name.map_name (K mx_name) raw_b;
   76.51 -        val c = full_binding thy b;
   76.52 +        val b = Binding.map_base (K mx_name) raw_b;
   76.53 +        val c = full_name thy b;
   76.54          val c_syn = if authentic then Syntax.constN ^ c else Name.name_of b;
   76.55          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
   76.56 -          cat_error msg ("in declaration of constant " ^ quote (Name.display b));
   76.57 +          cat_error msg ("in declaration of constant " ^ quote (Binding.display b));
   76.58          val T' = Logic.varifyT T;
   76.59        in ((b, T'), (c_syn, T', mx), Const (c, T)) end;
   76.60      val args = map prep raw_args;
   76.61 @@ -526,7 +525,7 @@
   76.62      |> pair (map #3 args)
   76.63    end;
   76.64  
   76.65 -fun bindify (name, T, mx) = (Name.binding name, T, mx);
   76.66 +fun bindify (name, T, mx) = (Binding.name name, T, mx);
   76.67  
   76.68  in
   76.69  
   76.70 @@ -551,7 +550,7 @@
   76.71      val pp = Syntax.pp_global thy;
   76.72      val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
   76.73      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
   76.74 -      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Name.display b));
   76.75 +      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.display b));
   76.76      val (res, consts') = consts_of thy
   76.77        |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (b, t);
   76.78    in (res, thy |> map_consts (K consts')) end;
    77.1 --- a/src/Pure/simplifier.ML	Wed Dec 03 21:00:39 2008 -0800
    77.2 +++ b/src/Pure/simplifier.ML	Thu Dec 04 14:43:33 2008 +0100
    77.3 @@ -194,11 +194,11 @@
    77.4    in
    77.5      lthy |> LocalTheory.declaration (fn phi =>
    77.6        let
    77.7 -        val b' = Morphism.name phi (Name.binding name);
    77.8 +        val b' = Morphism.binding phi (Binding.name name);
    77.9          val simproc' = morph_simproc phi simproc;
   77.10        in
   77.11          Simprocs.map (fn simprocs =>
   77.12 -          NameSpace.table_declare naming (b', simproc') simprocs |> snd
   77.13 +          NameSpace.bind naming (b', simproc') simprocs |> snd
   77.14              handle Symtab.DUP dup => err_dup_simproc dup)
   77.15          #> map_ss (fn ss => ss addsimprocs [simproc'])
   77.16        end)
    78.1 --- a/src/Pure/theory.ML	Wed Dec 03 21:00:39 2008 -0800
    78.2 +++ b/src/Pure/theory.ML	Thu Dec 04 14:43:33 2008 +0100
    78.3 @@ -36,7 +36,7 @@
    78.4    val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory
    78.5    val add_finals: bool -> string list -> theory -> theory
    78.6    val add_finals_i: bool -> term list -> theory -> theory
    78.7 -  val specify_const: Properties.T -> (Name.binding * typ) * mixfix -> theory -> term * theory
    78.8 +  val specify_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory
    78.9  end
   78.10  
   78.11  structure Theory: THEORY =
   78.12 @@ -253,7 +253,7 @@
   78.13  fun check_def thy unchecked overloaded (bname, tm) defs =
   78.14    let
   78.15      val ctxt = ProofContext.init thy;
   78.16 -    val name = Sign.full_name thy bname;
   78.17 +    val name = Sign.full_bname thy bname;
   78.18      val (lhs_const, rhs) = Sign.cert_def ctxt tm;
   78.19      val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
   78.20      val _ = check_overloading thy overloaded lhs_const;
    79.1 --- a/src/Pure/thm.ML	Wed Dec 03 21:00:39 2008 -0800
    79.2 +++ b/src/Pure/thm.ML	Thu Dec 04 14:43:33 2008 +0100
    79.3 @@ -1732,9 +1732,9 @@
    79.4  fun add_oracle (bname, oracle) thy =
    79.5    let
    79.6      val naming = Sign.naming_of thy;
    79.7 -    val name = NameSpace.full naming bname;
    79.8 +    val name = NameSpace.full_name naming (Binding.name bname);
    79.9      val thy' = thy |> Oracles.map (fn (space, tab) =>
   79.10 -      (NameSpace.declare naming name space,
   79.11 +      (NameSpace.declare_base naming name space,
   79.12          Symtab.update_new (name, stamp ()) tab handle Symtab.DUP dup => err_dup_ora dup));
   79.13    in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
   79.14  
    80.1 --- a/src/Pure/type.ML	Wed Dec 03 21:00:39 2008 -0800
    80.2 +++ b/src/Pure/type.ML	Thu Dec 04 14:43:33 2008 +0100
    80.3 @@ -509,10 +509,10 @@
    80.4  fun add_class pp naming (c, cs) tsig =
    80.5    tsig |> map_tsig (fn ((space, classes), default, types) =>
    80.6      let
    80.7 -      val c' = NameSpace.full naming c;
    80.8 +      val c' = NameSpace.full_name naming (Binding.name c);
    80.9        val cs' = map (cert_class tsig) cs
   80.10          handle TYPE (msg, _, _) => error msg;
   80.11 -      val space' = space |> NameSpace.declare naming c';
   80.12 +      val space' = space |> NameSpace.declare_base naming c';
   80.13        val classes' = classes |> Sorts.add_class pp (c', cs');
   80.14      in ((space', classes'), default, types) end);
   80.15  
   80.16 @@ -568,8 +568,8 @@
   80.17  fun new_decl naming tags (c, decl) (space, types) =
   80.18    let
   80.19      val tags' = tags |> Position.default_properties (Position.thread_data ());
   80.20 -    val c' = NameSpace.full naming c;
   80.21 -    val space' = NameSpace.declare naming c' space;
   80.22 +    val c' = NameSpace.full_name naming (Binding.name c);
   80.23 +    val space' = NameSpace.declare_base naming c' space;
   80.24      val types' =
   80.25        (case Symtab.lookup types c' of
   80.26          SOME ((decl', _), _) => err_in_decls c' decl decl'
    81.1 --- a/src/Pure/variable.ML	Wed Dec 03 21:00:39 2008 -0800
    81.2 +++ b/src/Pure/variable.ML	Thu Dec 04 14:43:33 2008 +0100
    81.3 @@ -398,7 +398,7 @@
    81.4      val fact = export inner outer;
    81.5      val term = singleton (export_terms inner outer);
    81.6      val typ = Logic.type_map term;
    81.7 -  in Morphism.morphism {name = I, var = I, typ = typ, term = term, fact = fact} end;
    81.8 +  in Morphism.morphism {binding = I, var = I, typ = typ, term = term, fact = fact} end;
    81.9  
   81.10  
   81.11  
    82.1 --- a/src/Tools/induct.ML	Wed Dec 03 21:00:39 2008 -0800
    82.2 +++ b/src/Tools/induct.ML	Thu Dec 04 14:43:33 2008 +0100
    82.3 @@ -1,5 +1,4 @@
    82.4  (*  Title:      Tools/induct.ML
    82.5 -    ID:         $Id$
    82.6      Author:     Markus Wenzel, TU Muenchen
    82.7  
    82.8  Proof by cases, induction, and coinduction.
    82.9 @@ -51,7 +50,7 @@
   82.10    val setN: string
   82.11    (*proof methods*)
   82.12    val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
   82.13 -  val add_defs: (Name.binding option * term) option list -> Proof.context ->
   82.14 +  val add_defs: (Binding.T option * term) option list -> Proof.context ->
   82.15      (term option list * thm list) * Proof.context
   82.16    val atomize_term: theory -> term -> term
   82.17    val atomize_tac: int -> tactic
   82.18 @@ -63,7 +62,7 @@
   82.19    val cases_tac: Proof.context -> term option list list -> thm option ->
   82.20      thm list -> int -> cases_tactic
   82.21    val get_inductT: Proof.context -> term option list list -> thm list list
   82.22 -  val induct_tac: Proof.context -> (Name.binding option * term) option list list ->
   82.23 +  val induct_tac: Proof.context -> (Binding.T option * term) option list list ->
   82.24      (string * typ) list list -> term option list -> thm list option ->
   82.25      thm list -> int -> cases_tactic
   82.26    val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
   82.27 @@ -553,7 +552,7 @@
   82.28    let
   82.29      fun add (SOME (SOME x, t)) ctxt =
   82.30            let val ([(lhs, (_, th))], ctxt') =
   82.31 -            LocalDefs.add_defs [((x, NoSyn), ((Name.no_binding, []), t))] ctxt
   82.32 +            LocalDefs.add_defs [((x, NoSyn), ((Binding.empty, []), t))] ctxt
   82.33            in ((SOME lhs, [th]), ctxt') end
   82.34        | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
   82.35        | add NONE ctxt = ((NONE, []), ctxt);
    83.1 --- a/src/ZF/Tools/datatype_package.ML	Wed Dec 03 21:00:39 2008 -0800
    83.2 +++ b/src/ZF/Tools/datatype_package.ML	Thu Dec 04 14:43:33 2008 +0100
    83.3 @@ -101,7 +101,7 @@
    83.4    val npart = length rec_names;  (*number of mutually recursive parts*)
    83.5  
    83.6  
    83.7 -  val full_name = Sign.full_name thy_path;
    83.8 +  val full_name = Sign.full_bname thy_path;
    83.9  
   83.10    (*Make constructor definition;
   83.11      kpart is the number of this mutually recursive part*)
   83.12 @@ -262,7 +262,7 @@
   83.13               ||> add_recursor
   83.14               ||> Sign.parent_path
   83.15  
   83.16 -  val intr_names = map (Name.binding o #2) (List.concat con_ty_lists);
   83.17 +  val intr_names = map (Binding.name o #2) (List.concat con_ty_lists);
   83.18    val (thy1, ind_result) =
   83.19      thy0 |> Ind_Package.add_inductive_i
   83.20        false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms))
    84.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Dec 03 21:00:39 2008 -0800
    84.2 +++ b/src/ZF/Tools/inductive_package.ML	Thu Dec 04 14:43:33 2008 +0100
    84.3 @@ -29,10 +29,10 @@
    84.4    (*Insert definitions for the recursive sets, which
    84.5       must *already* be declared as constants in parent theory!*)
    84.6    val add_inductive_i: bool -> term list * term ->
    84.7 -    ((Name.binding * term) * attribute list) list ->
    84.8 +    ((Binding.T * term) * attribute list) list ->
    84.9      thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
   84.10    val add_inductive: string list * string ->
   84.11 -    ((Name.binding * string) * Attrib.src list) list ->
   84.12 +    ((Binding.T * string) * Attrib.src list) list ->
   84.13      (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
   84.14      (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list ->
   84.15      theory -> theory * inductive_result
    85.1 --- a/src/ZF/Tools/primrec_package.ML	Wed Dec 03 21:00:39 2008 -0800
    85.2 +++ b/src/ZF/Tools/primrec_package.ML	Thu Dec 04 14:43:33 2008 +0100
    85.3 @@ -9,8 +9,8 @@
    85.4  
    85.5  signature PRIMREC_PACKAGE =
    85.6  sig
    85.7 -  val add_primrec: ((Name.binding * string) * Attrib.src list) list -> theory -> theory * thm list
    85.8 -  val add_primrec_i: ((Name.binding * term) * attribute list) list -> theory -> theory * thm list
    85.9 +  val add_primrec: ((Binding.T * string) * Attrib.src list) list -> theory -> theory * thm list
   85.10 +  val add_primrec_i: ((Binding.T * term) * attribute list) list -> theory -> theory * thm list
   85.11  end;
   85.12  
   85.13  structure PrimrecPackage : PRIMREC_PACKAGE =
    86.1 --- a/src/ZF/ind_syntax.ML	Wed Dec 03 21:00:39 2008 -0800
    86.2 +++ b/src/ZF/ind_syntax.ML	Thu Dec 04 14:43:33 2008 +0100
    86.3 @@ -85,7 +85,7 @@
    86.4        Logic.list_implies
    86.5          (map FOLogic.mk_Trueprop prems,
    86.6  	 FOLogic.mk_Trueprop
    86.7 -	    (@{const mem} $ list_comb (Const (Sign.full_name sg name, T), args)
    86.8 +	    (@{const mem} $ list_comb (Const (Sign.full_bname sg name, T), args)
    86.9  	               $ rec_tm))
   86.10    in  map mk_intr constructs  end;
   86.11