more uniform handling of binding in packages;
authorwenzelm
Sat Mar 07 22:17:25 2009 +0100 (2009-03-07)
changeset 3034576fd85bbf139
parent 30344 10a67c5ddddb
child 30346 90efbb8a8cb2
more uniform handling of binding in packages;
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/function_package/size.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/inductive_set_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/typecopy_package.ML
src/HOL/Tools/typedef_package.ML
src/HOLCF/Tools/cont_consts.ML
src/HOLCF/Tools/domain/domain_extender.ML
src/HOLCF/Tools/pcpodef_package.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
src/ZF/ind_syntax.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Mar 07 22:16:50 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Mar 07 22:17:25 2009 +0100
     1.3 @@ -100,7 +100,7 @@
     1.4      
     1.5      val (_,thy1) = 
     1.6      fold_map (fn ak => fn thy => 
     1.7 -          let val dt = ([],ak,NoSyn,[(ak,[@{typ nat}],NoSyn)]) 
     1.8 +          let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
     1.9                val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype true false [ak] [dt] thy
    1.10                val inject_flat = Library.flat inject
    1.11                val ak_type = Type (Sign.intern_type thy1 ak,[])
    1.12 @@ -187,7 +187,7 @@
    1.13                      cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c)))
    1.14          val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
    1.15        in
    1.16 -        thy |> Sign.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)] 
    1.17 +        thy |> Sign.add_consts_i [(Binding.name ("swap_" ^ ak_name), swapT, NoSyn)] 
    1.18              |> PureThy.add_defs_unchecked true [((Binding.name name, def2),[])]
    1.19              |> snd
    1.20              |> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])]
    1.21 @@ -217,7 +217,7 @@
    1.22                     (Const (qu_prm_name, prmT) $ mk_Cons x xs $ a,
    1.23                      Const (swap_name, swapT) $ x $ (Const (qu_prm_name, prmT) $ xs $ a)));
    1.24        in
    1.25 -        thy |> Sign.add_consts_i [(prm_name, mk_permT T --> T --> T, NoSyn)] 
    1.26 +        thy |> Sign.add_consts_i [(Binding.name prm_name, mk_permT T --> T --> T, NoSyn)] 
    1.27              |> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1), []),(("", def2), [])]
    1.28        end) ak_names_types thy3;
    1.29      
    1.30 @@ -300,7 +300,7 @@
    1.31                         (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
    1.32                          HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
    1.33        in
    1.34 -          AxClass.define_class (cl_name, ["HOL.type"]) []
    1.35 +          AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
    1.36                  [((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
    1.37                   ((Binding.name (cl_name ^ "2"), []), [axiom2]),                           
    1.38                   ((Binding.name (cl_name ^ "3"), []), [axiom3])] thy
    1.39 @@ -349,7 +349,8 @@
    1.40            val axiom1   = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
    1.41  
    1.42         in  
    1.43 -        AxClass.define_class (cl_name, [pt_name]) [] [((Binding.name (cl_name ^ "1"), []), [axiom1])] thy            
    1.44 +        AxClass.define_class (Binding.name cl_name, [pt_name]) []
    1.45 +          [((Binding.name (cl_name ^ "1"), []), [axiom1])] thy
    1.46         end) ak_names_types thy8; 
    1.47           
    1.48       (* proves that every fs_<ak>-type together with <ak>-type   *)
    1.49 @@ -398,7 +399,7 @@
    1.50                             (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
    1.51                                             cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
    1.52                 in  
    1.53 -                 AxClass.define_class (cl_name, ["HOL.type"]) []
    1.54 +                 AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
    1.55                     [((Binding.name (cl_name ^ "1"), []), [ax1])] thy'  
    1.56                 end) ak_names_types thy) ak_names_types thy12;
    1.57  
     2.1 --- a/src/HOL/Nominal/nominal_package.ML	Sat Mar 07 22:16:50 2009 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_package.ML	Sat Mar 07 22:17:25 2009 +0100
     2.3 @@ -197,7 +197,7 @@
     2.4      val tmp_thy = thy |>
     2.5        Theory.copy |>
     2.6        Sign.add_types (map (fn (tvs, tname, mx, _) =>
     2.7 -        (tname, length tvs, mx)) dts);
     2.8 +        (Binding.name tname, length tvs, mx)) dts);
     2.9  
    2.10      val atoms = atoms_of thy;
    2.11  
    2.12 @@ -235,8 +235,8 @@
    2.13            Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
    2.14        | replace_types T = T;
    2.15  
    2.16 -    val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, tname ^ "_Rep", NoSyn,
    2.17 -      map (fn (cname, cargs, mx) => (cname ^ "_Rep",
    2.18 +    val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, Binding.name (tname ^ "_Rep"), NoSyn,
    2.19 +      map (fn (cname, cargs, mx) => (Binding.name (cname ^ "_Rep"),
    2.20          map replace_types cargs, NoSyn)) constrs)) dts';
    2.21  
    2.22      val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
    2.23 @@ -615,7 +615,8 @@
    2.24      val (typedefs, thy6) =
    2.25        thy4
    2.26        |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
    2.27 -          TypedefPackage.add_typedef false (SOME name') (name, map fst tvs, mx)
    2.28 +          TypedefPackage.add_typedef false (SOME (Binding.name name'))
    2.29 +            (Binding.name name, map fst tvs, mx)
    2.30              (Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
    2.31                 Const (cname, U --> HOLogic.boolT)) NONE
    2.32              (rtac exI 1 THEN rtac CollectI 1 THEN
    2.33 @@ -800,7 +801,7 @@
    2.34            (Const (rep_name, T --> T') $ lhs, rhs));
    2.35          val def_name = (NameSpace.base_name cname) ^ "_def";
    2.36          val ([def_thm], thy') = thy |>
    2.37 -          Sign.add_consts_i [(cname', constrT, mx)] |>
    2.38 +          Sign.add_consts_i [(Binding.name cname', constrT, mx)] |>
    2.39            (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
    2.40        in (thy', defs @ [def_thm], eqns @ [eqn]) end;
    2.41  
    2.42 @@ -2012,7 +2013,7 @@
    2.43      val (reccomb_defs, thy12) =
    2.44        thy11
    2.45        |> Sign.add_consts_i (map (fn ((name, T), T') =>
    2.46 -          (NameSpace.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn))
    2.47 +          (Binding.name (NameSpace.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
    2.48            (reccomb_names ~~ recTs ~~ rec_result_Ts))
    2.49        |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
    2.50            (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
     3.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Sat Mar 07 22:16:50 2009 +0100
     3.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sat Mar 07 22:17:25 2009 +0100
     3.3 @@ -235,7 +235,7 @@
     3.4      val (reccomb_defs, thy2) =
     3.5        thy1
     3.6        |> Sign.add_consts_i (map (fn ((name, T), T') =>
     3.7 -          (NameSpace.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
     3.8 +          (Binding.name (NameSpace.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
     3.9            (reccomb_names ~~ recTs ~~ rec_result_Ts))
    3.10        |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
    3.11            (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
     4.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Mar 07 22:16:50 2009 +0100
     4.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Mar 07 22:17:25 2009 +0100
     4.3 @@ -36,8 +36,8 @@
     4.4         simps : thm list} -> Proof.context -> Proof.context) -> string list option -> term list
     4.5      -> theory -> Proof.state;
     4.6    val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state;
     4.7 -  val add_datatype : bool -> bool -> string list -> (string list * bstring * mixfix *
     4.8 -    (bstring * typ list * mixfix) list) list -> theory ->
     4.9 +  val add_datatype : bool -> bool -> string list -> (string list * binding * mixfix *
    4.10 +    (binding * typ list * mixfix) list) list -> theory ->
    4.11        {distinct : thm list list,
    4.12         inject : thm list list,
    4.13         exhaustion : thm list,
    4.14 @@ -46,8 +46,8 @@
    4.15         split_thms : (thm * thm) list,
    4.16         induction : thm,
    4.17         simps : thm list} * theory
    4.18 -  val add_datatype_cmd : bool -> string list -> (string list * bstring * mixfix *
    4.19 -    (bstring * string list * mixfix) list) list -> theory ->
    4.20 +  val add_datatype_cmd : bool -> string list -> (string list * binding * mixfix *
    4.21 +    (binding * string list * mixfix) list) list -> theory ->
    4.22        {distinct : thm list list,
    4.23         inject : thm list list,
    4.24         exhaustion : thm list,
    4.25 @@ -566,11 +566,11 @@
    4.26  
    4.27      val (tyvars, _, _, _)::_ = dts;
    4.28      val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
    4.29 -      let val full_tname = Sign.full_bname tmp_thy (Syntax.type_name tname mx)
    4.30 +      let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
    4.31        in (case duplicates (op =) tvs of
    4.32              [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
    4.33                    else error ("Mutually recursive datatypes must have same type parameters")
    4.34 -          | dups => error ("Duplicate parameter(s) for datatype " ^ full_tname ^
    4.35 +          | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
    4.36                " : " ^ commas dups))
    4.37        end) dts);
    4.38  
    4.39 @@ -585,13 +585,14 @@
    4.40              val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
    4.41                  [] => ()
    4.42                | vs => error ("Extra type variables on rhs: " ^ commas vs))
    4.43 -          in (constrs @ [((if flat_names then Sign.full_bname tmp_thy else
    4.44 -                Sign.full_bname_path tmp_thy tname) (Syntax.const_name cname mx'),
    4.45 +          in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
    4.46 +                Sign.full_name_path tmp_thy (Binding.name_of tname))
    4.47 +                  (Binding.map_name (Syntax.const_name mx') cname),
    4.48                     map (dtyp_of_typ new_dts) cargs')],
    4.49                constr_syntax' @ [(cname, mx')], sorts'')
    4.50 -          end handle ERROR msg =>
    4.51 -            cat_error msg ("The error above occured in constructor " ^ cname ^
    4.52 -              " of datatype " ^ tname);
    4.53 +          end handle ERROR msg => cat_error msg
    4.54 +           ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^
    4.55 +            " of datatype " ^ quote (Binding.str_of tname));
    4.56  
    4.57          val (constrs', constr_syntax', sorts') =
    4.58            fold prep_constr constrs ([], [], sorts)
    4.59 @@ -599,11 +600,11 @@
    4.60        in
    4.61          case duplicates (op =) (map fst constrs') of
    4.62             [] =>
    4.63 -             (dts' @ [(i, (Sign.full_bname tmp_thy (Syntax.type_name tname mx),
    4.64 +             (dts' @ [(i, (Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname),
    4.65                  map DtTFree tvs, constrs'))],
    4.66                constr_syntax @ [constr_syntax'], sorts', i + 1)
    4.67           | dups => error ("Duplicate constructors " ^ commas dups ^
    4.68 -             " in datatype " ^ tname)
    4.69 +             " in datatype " ^ quote (Binding.str_of tname))
    4.70        end;
    4.71  
    4.72      val (dts', constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0);
    4.73 @@ -676,12 +677,13 @@
    4.74  local structure P = OuterParse and K = OuterKeyword in
    4.75  
    4.76  val datatype_decl =
    4.77 -  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
    4.78 -    (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
    4.79 +  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
    4.80 +    (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix));
    4.81  
    4.82  fun mk_datatype args =
    4.83    let
    4.84 -    val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
    4.85 +    val names = map
    4.86 +      (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args;
    4.87      val specs = map (fn ((((_, vs), t), mx), cons) =>
    4.88        (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
    4.89    in snd o add_datatype_cmd false names specs end;
     5.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Sat Mar 07 22:16:50 2009 +0100
     5.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sat Mar 07 22:17:25 2009 +0100
     5.3 @@ -15,7 +15,7 @@
     5.4    val distinctness_limit_setup : theory -> theory
     5.5    val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
     5.6      string list -> DatatypeAux.descr list -> (string * sort) list ->
     5.7 -      (string * mixfix) list -> (string * mixfix) list list -> attribute
     5.8 +      (binding * mixfix) list -> (binding * mixfix) list list -> attribute
     5.9          -> theory -> (thm list list * thm list list * thm list list *
    5.10            DatatypeAux.simproc_dist list * thm) * theory
    5.11  end;
    5.12 @@ -192,7 +192,7 @@
    5.13      val (typedefs, thy3) = thy2 |>
    5.14        parent_path flat_names |>
    5.15        fold_map (fn ((((name, mx), tvs), c), name') =>
    5.16 -          TypedefPackage.add_typedef false (SOME name') (name, tvs, mx)
    5.17 +          TypedefPackage.add_typedef false (SOME (Binding.name name')) (name, tvs, mx)
    5.18              (Collect $ Const (c, UnivT')) NONE
    5.19              (rtac exI 1 THEN rtac CollectI 1 THEN
    5.20                QUIET_BREADTH_FIRST (has_fewer_prems 1)
    5.21 @@ -212,7 +212,7 @@
    5.22  
    5.23      (* isomorphism declarations *)
    5.24  
    5.25 -    val iso_decls = map (fn (T, s) => (s, T --> Univ_elT, NoSyn))
    5.26 +    val iso_decls = map (fn (T, s) => (Binding.name s, T --> Univ_elT, NoSyn))
    5.27        (oldTs ~~ rep_names');
    5.28  
    5.29      (* constructor definitions *)
     6.1 --- a/src/HOL/Tools/function_package/size.ML	Sat Mar 07 22:16:50 2009 +0100
     6.2 +++ b/src/HOL/Tools/function_package/size.ML	Sat Mar 07 22:17:25 2009 +0100
     6.3 @@ -140,7 +140,7 @@
     6.4      val ((size_def_thms, size_def_thms'), thy') =
     6.5        thy
     6.6        |> Sign.add_consts_i (map (fn (s, T) =>
     6.7 -           (NameSpace.base_name s, param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
     6.8 +           (Binding.name (NameSpace.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
     6.9             (size_names ~~ recTs1))
    6.10        |> PureThy.add_defs false
    6.11          (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
     7.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Mar 07 22:16:50 2009 +0100
     7.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Mar 07 22:17:25 2009 +0100
     7.3 @@ -68,8 +68,8 @@
     7.4      val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
     7.5        (Logic.strip_imp_concl (prop_of (hd intrs))));
     7.6      val params = map dest_Var (Library.take (nparms, ts));
     7.7 -    val tname = space_implode "_" (NameSpace.base_name s ^ "T" :: vs);
     7.8 -    fun constr_of_intr intr = (NameSpace.base_name (name_of_thm intr),
     7.9 +    val tname = Binding.name (space_implode "_" (NameSpace.base_name s ^ "T" :: vs));
    7.10 +    fun constr_of_intr intr = (Binding.name (NameSpace.base_name (name_of_thm intr)),
    7.11        map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
    7.12          filter_out (equal Extraction.nullT) (map
    7.13            (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
    7.14 @@ -234,7 +234,7 @@
    7.15    end;
    7.16  
    7.17  fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
    7.18 -  if (name: string) = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
    7.19 +  if Binding.eq_name (name, s) then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
    7.20    else x;
    7.21  
    7.22  fun add_dummies f [] _ thy =
    7.23 @@ -242,14 +242,14 @@
    7.24    | add_dummies f dts used thy =
    7.25        thy
    7.26        |> f (map snd dts)
    7.27 -      |-> (fn dtinfo => pair ((map fst dts), SOME dtinfo))
    7.28 +      |-> (fn dtinfo => pair (map fst dts, SOME dtinfo))
    7.29      handle DatatypeAux.Datatype_Empty name' =>
    7.30        let
    7.31          val name = NameSpace.base_name name';
    7.32 -        val dname = Name.variant used "Dummy"
    7.33 +        val dname = Name.variant used "Dummy";
    7.34        in
    7.35          thy
    7.36 -        |> add_dummies f (map (add_dummy name dname) dts) (dname :: used)
    7.37 +        |> add_dummies f (map (add_dummy (Binding.name name) (Binding.name dname)) dts) (dname :: used)
    7.38        end;
    7.39  
    7.40  fun mk_realizer thy vs (name, rule, rrule, rlz, rt) =
    7.41 @@ -296,7 +296,7 @@
    7.42  
    7.43      val thy1' = thy1 |>
    7.44        Theory.copy |>
    7.45 -      Sign.add_types (map (fn s => (NameSpace.base_name s, ar, NoSyn)) tnames) |>
    7.46 +      Sign.add_types (map (fn s => (Binding.name (NameSpace.base_name s), ar, NoSyn)) tnames) |>
    7.47        fold (fn s => AxClass.axiomatize_arity
    7.48          (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
    7.49          Extraction.add_typeof_eqns_i ty_eqs;
    7.50 @@ -308,7 +308,7 @@
    7.51      val ((dummies, dt_info), thy2) =
    7.52        thy1
    7.53        |> add_dummies
    7.54 -           (DatatypePackage.add_datatype false false (map #2 dts))
    7.55 +           (DatatypePackage.add_datatype false false (map (Binding.name_of o #2) dts))
    7.56             (map (pair false) dts) []
    7.57        ||> Extraction.add_typeof_eqns_i ty_eqs
    7.58        ||> Extraction.add_realizes_eqns_i rlz_eqs;
    7.59 @@ -330,14 +330,17 @@
    7.60          (if c = Extraction.nullt then c else list_comb (c, map Var (rev
    7.61            (Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr)))
    7.62              (maps snd rss ~~ List.concat constrss);
    7.63 -    val (rlzpreds, rlzpreds') = split_list
    7.64 -      (distinct (op = o pairself (#1 o #1)) (map (fn rintr =>
    7.65 +    val (rlzpreds, rlzpreds') =
    7.66 +      rintrs |> map (fn rintr =>
    7.67          let
    7.68 -          val Const (s, T) = head_of (HOLogic.dest_Trueprop
    7.69 -            (Logic.strip_assums_concl rintr));
    7.70 +          val Const (s, T) = head_of (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr));
    7.71            val s' = NameSpace.base_name s;
    7.72 -          val T' = Logic.unvarifyT T
    7.73 -        in (((Binding.name s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
    7.74 +          val T' = Logic.unvarifyT T;
    7.75 +        in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end)
    7.76 +      |> distinct (op = o pairself (#1 o #1))
    7.77 +      |> map (apfst (apfst (apfst Binding.name)))
    7.78 +      |> split_list;
    7.79 +
    7.80      val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
    7.81        (List.take (snd (strip_comb
    7.82          (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
     8.1 --- a/src/HOL/Tools/inductive_set_package.ML	Sat Mar 07 22:16:50 2009 +0100
     8.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Sat Mar 07 22:17:25 2009 +0100
     8.3 @@ -464,7 +464,7 @@
     8.4             | NONE => u)) |>
     8.5          Pattern.rewrite_term thy [] [to_pred_proc thy eqns'] |>
     8.6          eta_contract (member op = cs' orf is_pred pred_arities))) intros;
     8.7 -    val cnames_syn' = map (fn (b, _) => (Binding.map_name (suffix "p") b, NoSyn)) cnames_syn;
     8.8 +    val cnames_syn' = map (fn (b, _) => (Binding.suffix_name "p" b, NoSyn)) cnames_syn;
     8.9      val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
    8.10      val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
    8.11        InductivePackage.add_ind_def
     9.1 --- a/src/HOL/Tools/record_package.ML	Sat Mar 07 22:16:50 2009 +0100
     9.2 +++ b/src/HOL/Tools/record_package.ML	Sat Mar 07 22:17:25 2009 +0100
     9.3 @@ -1461,9 +1461,10 @@
     9.4            Abs_inject=abs_inject, Abs_inverse = abs_inverse, ...} = TypedefPackage.get_info thy name;
     9.5          val rewrite_rule = MetaSimplifier.rewrite_rule [rec_UNIV_I, rec_True_simp];
     9.6        in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end;
     9.7 +    val tname = Binding.name (NameSpace.base_name name);
     9.8    in
     9.9      thy
    9.10 -    |> TypecopyPackage.add_typecopy (suffix ext_typeN (NameSpace.base_name name), alphas) repT NONE
    9.11 +    |> TypecopyPackage.add_typecopy (Binding.suffix_name ext_typeN tname, alphas) repT NONE
    9.12      |-> (fn (name, _) => `(fn thy => get_thms thy name))
    9.13    end;
    9.14  
    9.15 @@ -1531,9 +1532,9 @@
    9.16      (* 1st stage: defs_thy *)
    9.17      fun mk_defs () =
    9.18        thy
    9.19 -      |> extension_typedef name repT (alphas@[zeta])
    9.20 +      |> extension_typedef name repT (alphas @ [zeta])
    9.21        ||> Sign.add_consts_i
    9.22 -            (map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
    9.23 +            (map (Syntax.no_syn o apfst Binding.name) (apfst base ext_decl :: dest_decls @ upd_decls))
    9.24        ||>> PureThy.add_defs false
    9.25              (map (Thm.no_attributes o apfst Binding.name) (ext_spec :: dest_specs))
    9.26        ||>> PureThy.add_defs false
    9.27 @@ -1895,8 +1896,8 @@
    9.28  
    9.29      (*record (scheme) type abbreviation*)
    9.30      val recordT_specs =
    9.31 -      [(suffix schemeN bname, alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
    9.32 -        (bname, alphas, recT0, Syntax.NoSyn)];
    9.33 +      [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
    9.34 +        (Binding.name bname, alphas, recT0, Syntax.NoSyn)];
    9.35  
    9.36      (*selectors*)
    9.37      fun mk_sel_spec (c,T) =
    9.38 @@ -1937,8 +1938,9 @@
    9.39        |> Sign.add_tyabbrs_i recordT_specs
    9.40        |> Sign.add_path bname
    9.41        |> Sign.add_consts_i
    9.42 -          (map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
    9.43 -      |> (Sign.add_consts_i o map Syntax.no_syn)
    9.44 +          (map2 (fn (x, T) => fn mx => (Binding.name x, T, mx))
    9.45 +            sel_decls (field_syntax @ [Syntax.NoSyn]))
    9.46 +      |> (Sign.add_consts_i o map (fn (x, T) => (Binding.name x, T, Syntax.NoSyn)))
    9.47            (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
    9.48        |> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) sel_specs)
    9.49        ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) upd_specs)
    10.1 --- a/src/HOL/Tools/typecopy_package.ML	Sat Mar 07 22:16:50 2009 +0100
    10.2 +++ b/src/HOL/Tools/typecopy_package.ML	Sat Mar 07 22:17:25 2009 +0100
    10.3 @@ -14,7 +14,7 @@
    10.4      proj: string * typ,
    10.5      proj_def: thm
    10.6    }
    10.7 -  val add_typecopy: bstring * string list -> typ -> (bstring * bstring) option
    10.8 +  val add_typecopy: binding * string list -> typ -> (binding * binding) option
    10.9      -> theory -> (string * info) * theory
   10.10    val get_typecopies: theory -> string list
   10.11    val get_info: theory -> string -> info option
    11.1 --- a/src/HOL/Tools/typedef_package.ML	Sat Mar 07 22:16:50 2009 +0100
    11.2 +++ b/src/HOL/Tools/typedef_package.ML	Sat Mar 07 22:17:25 2009 +0100
    11.3 @@ -13,12 +13,12 @@
    11.4      Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
    11.5      Rep_induct: thm, Abs_induct: thm}
    11.6    val get_info: theory -> string -> info option
    11.7 -  val add_typedef: bool -> string option -> bstring * string list * mixfix ->
    11.8 -    term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory
    11.9 -  val typedef: (bool * string) * (bstring * string list * mixfix) * term
   11.10 -    * (string * string) option -> theory -> Proof.state
   11.11 -  val typedef_cmd: (bool * string) * (bstring * string list * mixfix) * string
   11.12 -    * (string * string) option -> theory -> Proof.state
   11.13 +  val add_typedef: bool -> binding option -> binding * string list * mixfix ->
   11.14 +    term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
   11.15 +  val typedef: (bool * binding) * (binding * string list * mixfix) * term
   11.16 +    * (binding * binding) option -> theory -> Proof.state
   11.17 +  val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string
   11.18 +    * (binding * binding) option -> theory -> Proof.state
   11.19    val interpretation: (string -> theory -> theory) -> theory -> theory
   11.20    val setup: theory -> theory
   11.21  end;
   11.22 @@ -51,9 +51,6 @@
   11.23  
   11.24  (* prepare_typedef *)
   11.25  
   11.26 -fun err_in_typedef msg name =
   11.27 -  cat_error msg ("The error(s) above occurred in typedef " ^ quote name);
   11.28 -
   11.29  fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
   11.30  
   11.31  structure TypedefInterpretation = InterpretationFun(type T = string val eq = op =);
   11.32 @@ -63,10 +60,12 @@
   11.33    let
   11.34      val _ = Theory.requires thy "Typedef" "typedefs";
   11.35      val ctxt = ProofContext.init thy;
   11.36 -    val full = Sign.full_bname thy;
   11.37 +
   11.38 +    val full = Sign.full_name thy;
   11.39 +    val full_name = full name;
   11.40 +    val bname = Binding.name_of name;
   11.41  
   11.42      (*rhs*)
   11.43 -    val full_name = full name;
   11.44      val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
   11.45      val setT = Term.fastype_of set;
   11.46      val rhs_tfrees = Term.add_tfrees set [];
   11.47 @@ -81,11 +80,14 @@
   11.48        |> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT))
   11.49        |> map TFree;
   11.50  
   11.51 -    val tname = Syntax.type_name t mx;
   11.52 +    val tname = Binding.map_name (Syntax.type_name mx) t;
   11.53      val full_tname = full tname;
   11.54      val newT = Type (full_tname, map TFree lhs_tfrees);
   11.55  
   11.56 -    val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
   11.57 +    val (Rep_name, Abs_name) =
   11.58 +      (case opt_morphs of
   11.59 +        NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
   11.60 +      | SOME morphs => morphs);
   11.61      val setT' = map Term.itselfT args_setT ---> setT;
   11.62      val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT);
   11.63      val RepC = Const (full Rep_name, newT --> oldT);
   11.64 @@ -97,15 +99,15 @@
   11.65      val set' = if def then setC else set;
   11.66      val goal' = mk_inhabited set';
   11.67      val goal = mk_inhabited set;
   11.68 -    val goal_pat = mk_inhabited (Var (the_default (name, 0) (Syntax.read_variable name), setT));
   11.69 +    val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Syntax.read_variable bname), setT));
   11.70  
   11.71      (*axiomatization*)
   11.72 -    val typedef_name = "type_definition_" ^ name;
   11.73 +    val typedef_name = Binding.prefix_name "type_definition_" name;
   11.74      val typedefC =
   11.75        Const (@{const_name type_definition},
   11.76          (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
   11.77      val typedef_prop = Logic.mk_implies (goal', HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set'));
   11.78 -    val typedef_deps = Term.fold_aterms (fn Const c => insert (op =) c | _ => I) set' [];
   11.79 +    val typedef_deps = Term.add_consts set' [];
   11.80  
   11.81      (*set definition*)
   11.82      fun add_def theory =
   11.83 @@ -131,7 +133,7 @@
   11.84           (Abs_name, oldT --> newT, NoSyn)]
   11.85        #> add_def
   11.86        #-> (fn set_def =>
   11.87 -        PureThy.add_axioms [((Binding.name typedef_name, typedef_prop),
   11.88 +        PureThy.add_axioms [((typedef_name, typedef_prop),
   11.89            [Thm.rule_attribute (K (fn cond_axm => contract_def set_def inhabited RS cond_axm))])]
   11.90          ##>> pair set_def)
   11.91        ##> Theory.add_deps "" (dest_Const RepC) typedef_deps
   11.92 @@ -142,21 +144,21 @@
   11.93            val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
   11.94                Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) =
   11.95              thy1
   11.96 -            |> Sign.add_path name
   11.97 +            |> Sign.add_path (Binding.name_of name)
   11.98              |> PureThy.add_thms
   11.99 -              ((map o apfst o apfst) Binding.name [((Rep_name, make @{thm type_definition.Rep}), []),
  11.100 -                ((Rep_name ^ "_inverse", make @{thm type_definition.Rep_inverse}), []),
  11.101 -                ((Abs_name ^ "_inverse", make @{thm type_definition.Abs_inverse}), []),
  11.102 -                ((Rep_name ^ "_inject", make @{thm type_definition.Rep_inject}), []),
  11.103 -                ((Abs_name ^ "_inject", make @{thm type_definition.Abs_inject}), []),
  11.104 -                ((Rep_name ^ "_cases", make @{thm type_definition.Rep_cases}),
  11.105 -                  [RuleCases.case_names [Rep_name], Induct.cases_pred full_name]),
  11.106 -                ((Abs_name ^ "_cases", make @{thm type_definition.Abs_cases}),
  11.107 -                  [RuleCases.case_names [Abs_name], Induct.cases_type full_tname]),
  11.108 -                ((Rep_name ^ "_induct", make @{thm type_definition.Rep_induct}),
  11.109 -                  [RuleCases.case_names [Rep_name], Induct.induct_pred full_name]),
  11.110 -                ((Abs_name ^ "_induct", make @{thm type_definition.Abs_induct}),
  11.111 -                  [RuleCases.case_names [Abs_name], Induct.induct_type full_tname])])
  11.112 +              [((Rep_name, make @{thm type_definition.Rep}), []),
  11.113 +                ((Binding.suffix_name "_inverse" Rep_name, make @{thm type_definition.Rep_inverse}), []),
  11.114 +                ((Binding.suffix_name "_inverse" Abs_name, make @{thm type_definition.Abs_inverse}), []),
  11.115 +                ((Binding.suffix_name "_inject" Rep_name, make @{thm type_definition.Rep_inject}), []),
  11.116 +                ((Binding.suffix_name "_inject" Abs_name, make @{thm type_definition.Abs_inject}), []),
  11.117 +                ((Binding.suffix_name "_cases" Rep_name, make @{thm type_definition.Rep_cases}),
  11.118 +                  [RuleCases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
  11.119 +                ((Binding.suffix_name "_cases" Abs_name, make @{thm type_definition.Abs_cases}),
  11.120 +                  [RuleCases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]),
  11.121 +                ((Binding.suffix_name "_induct" Rep_name, make @{thm type_definition.Rep_induct}),
  11.122 +                  [RuleCases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
  11.123 +                ((Binding.suffix_name "_induct" Abs_name, make @{thm type_definition.Abs_induct}),
  11.124 +                  [RuleCases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname])]
  11.125              ||> Sign.parent_path;
  11.126            val info = {rep_type = oldT, abs_type = newT,
  11.127              Rep_name = full Rep_name, Abs_name = full Abs_name,
  11.128 @@ -201,7 +203,8 @@
  11.129        |> typedef_result (setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal);
  11.130  
  11.131    in (set, goal, goal_pat, typedef_result) end
  11.132 -  handle ERROR msg => err_in_typedef msg name;
  11.133 +  handle ERROR msg =>
  11.134 +    cat_error msg ("The error(s) above occurred in typedef " ^ quote (Binding.str_of name));
  11.135  
  11.136  
  11.137  (* add_typedef: tactic interface *)
  11.138 @@ -245,13 +248,14 @@
  11.139  
  11.140  val typedef_decl =
  11.141    Scan.optional (P.$$$ "(" |--
  11.142 -      ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
  11.143 +      ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
  11.144          --| P.$$$ ")") (true, NONE) --
  11.145 -    (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
  11.146 -    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
  11.147 +    (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
  11.148 +    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
  11.149  
  11.150  fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
  11.151 -  typedef_cmd ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
  11.152 +  typedef_cmd ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name),
  11.153 +    (t, vs, mx), A, morphs);
  11.154  
  11.155  val _ =
  11.156    OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)"
    12.1 --- a/src/HOLCF/Tools/cont_consts.ML	Sat Mar 07 22:16:50 2009 +0100
    12.2 +++ b/src/HOLCF/Tools/cont_consts.ML	Sat Mar 07 22:17:25 2009 +0100
    12.3 @@ -52,11 +52,11 @@
    12.4     is generated and connected to the other declaration via some translation.
    12.5  *)
    12.6  fun fix_mixfix (syn                     , T, mx as Infix           p ) =
    12.7 -               (Syntax.const_name syn mx, T,       InfixName (syn, p))
    12.8 +               (Syntax.const_name mx syn, T,       InfixName (syn, p))
    12.9    | fix_mixfix (syn                     , T, mx as Infixl           p ) =
   12.10 -               (Syntax.const_name syn mx, T,       InfixlName (syn, p))
   12.11 +               (Syntax.const_name mx syn, T,       InfixlName (syn, p))
   12.12    | fix_mixfix (syn                     , T, mx as Infixr           p ) =
   12.13 -               (Syntax.const_name syn mx, T,       InfixrName (syn, p))
   12.14 +               (Syntax.const_name mx syn, T,       InfixrName (syn, p))
   12.15    | fix_mixfix decl = decl;
   12.16  fun transform decl = let
   12.17          val (c, T, mx) = fix_mixfix decl;
   12.18 @@ -73,7 +73,7 @@
   12.19  |   is_contconst (_,_,Binder _) = false
   12.20  |   is_contconst (c,T,mx      ) = cfun_arity T >= Syntax.mixfix_args mx
   12.21                           handle ERROR msg => cat_error msg ("in mixfix annotation for " ^
   12.22 -                                               quote (Syntax.const_name c mx));
   12.23 +                                               quote (Syntax.const_name mx c));
   12.24  
   12.25  
   12.26  (* add_consts(_i) *)
   12.27 @@ -85,10 +85,9 @@
   12.28      val transformed_decls = map transform contconst_decls;
   12.29    in
   12.30      thy
   12.31 -    |> Sign.add_consts_i normal_decls
   12.32 -    |> Sign.add_consts_i (map first transformed_decls)
   12.33 -    |> Sign.add_syntax_i (map second transformed_decls)
   12.34 -    |> Sign.add_trrules_i (List.concat (map third transformed_decls))
   12.35 +    |> (Sign.add_consts_i o map (upd_first Binding.name))
   12.36 +      (normal_decls @ map first transformed_decls @ map second transformed_decls)
   12.37 +    |> Sign.add_trrules_i (maps third transformed_decls)
   12.38    end;
   12.39  
   12.40  val add_consts = gen_add_consts Syntax.read_typ_global;
    13.1 --- a/src/HOLCF/Tools/domain/domain_extender.ML	Sat Mar 07 22:16:50 2009 +0100
    13.2 +++ b/src/HOLCF/Tools/domain/domain_extender.ML	Sat Mar 07 22:17:25 2009 +0100
    13.3 @@ -103,7 +103,7 @@
    13.4  			 (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs))
    13.5                     o fst) eqs''';
    13.6      val cons''' = map snd eqs''';
    13.7 -    fun thy_type  (dname,tvars)  = (NameSpace.base_name dname, length tvars, NoSyn);
    13.8 +    fun thy_type  (dname,tvars)  = (Binding.name (NameSpace.base_name dname), length tvars, NoSyn);
    13.9      fun thy_arity (dname,tvars)  = (dname, map (snd o dest_TFree) tvars, pcpoS);
   13.10      val thy'' = thy''' |> Sign.add_types     (map thy_type  dtnvs)
   13.11  		       |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
   13.12 @@ -119,7 +119,7 @@
   13.13        | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
   13.14        | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
   13.15      fun one_con (con,mx,args) =
   13.16 -	((Syntax.const_name con mx),
   13.17 +	((Syntax.const_name mx con),
   13.18  	 ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
   13.19  					find_index_eq tp dts,
   13.20  					DatatypeAux.dtyp_of_typ new_dts tp),
    14.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Sat Mar 07 22:16:50 2009 +0100
    14.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML	Sat Mar 07 22:17:25 2009 +0100
    14.3 @@ -7,14 +7,14 @@
    14.4  
    14.5  signature PCPODEF_PACKAGE =
    14.6  sig
    14.7 -  val pcpodef_proof: (bool * string) * (bstring * string list * mixfix) * term
    14.8 -    * (string * string) option -> theory -> Proof.state
    14.9 -  val pcpodef_proof_cmd: (bool * string) * (bstring * string list * mixfix) * string
   14.10 -    * (string * string) option -> theory -> Proof.state
   14.11 -  val cpodef_proof: (bool * string) * (bstring * string list * mixfix) * term
   14.12 -    * (string * string) option -> theory -> Proof.state
   14.13 -  val cpodef_proof_cmd: (bool * string) * (bstring * string list * mixfix) * string
   14.14 -    * (string * string) option -> theory -> Proof.state
   14.15 +  val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
   14.16 +    * (binding * binding) option -> theory -> Proof.state
   14.17 +  val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
   14.18 +    * (binding * binding) option -> theory -> Proof.state
   14.19 +  val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
   14.20 +    * (binding * binding) option -> theory -> Proof.state
   14.21 +  val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
   14.22 +    * (binding * binding) option -> theory -> Proof.state
   14.23  end;
   14.24  
   14.25  structure PcpodefPackage: PCPODEF_PACKAGE =
   14.26 @@ -24,9 +24,6 @@
   14.27  
   14.28  (* prepare_cpodef *)
   14.29  
   14.30 -fun err_in_cpodef msg name =
   14.31 -  cat_error msg ("The error(s) above occurred in cpodef " ^ quote name);
   14.32 -
   14.33  fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
   14.34  
   14.35  fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
   14.36 @@ -36,10 +33,12 @@
   14.37    let
   14.38      val _ = Theory.requires thy "Pcpodef" "pcpodefs";
   14.39      val ctxt = ProofContext.init thy;
   14.40 -    val full = Sign.full_bname thy;
   14.41 +
   14.42 +    val full = Sign.full_name thy;
   14.43 +    val full_name = full name;
   14.44 +    val bname = Binding.name_of name;
   14.45  
   14.46      (*rhs*)
   14.47 -    val full_name = full name;
   14.48      val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
   14.49      val setT = Term.fastype_of set;
   14.50      val rhs_tfrees = Term.add_tfrees set [];
   14.51 @@ -58,11 +57,14 @@
   14.52      val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
   14.53      val lhs_sorts = map snd lhs_tfrees;
   14.54  
   14.55 -    val tname = Syntax.type_name t mx;
   14.56 +    val tname = Binding.map_name (Syntax.type_name mx) t;
   14.57      val full_tname = full tname;
   14.58      val newT = Type (full_tname, map TFree lhs_tfrees);
   14.59  
   14.60 -    val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
   14.61 +    val (Rep_name, Abs_name) =
   14.62 +      (case opt_morphs of
   14.63 +        NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
   14.64 +      | SOME morphs => morphs);
   14.65      val RepC = Const (full Rep_name, newT --> oldT);
   14.66      fun lessC T = Const (@{const_name sq_le}, T --> T --> HOLogic.boolT);
   14.67      val less_def = Logic.mk_equals (lessC newT,
   14.68 @@ -76,7 +78,8 @@
   14.69            |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
   14.70          val less_def' = Syntax.check_term lthy3 less_def;
   14.71          val ((_, (_, less_definition')), lthy4) = lthy3
   14.72 -          |> Specification.definition (NONE, ((Binding.name ("less_" ^ name ^ "_def"), []), less_def'));
   14.73 +          |> Specification.definition (NONE,
   14.74 +              ((Binding.prefix_name "less_" (Binding.suffix_name "_def" name), []), less_def'));
   14.75          val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
   14.76          val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition';
   14.77          val thy5 = lthy4
   14.78 @@ -95,14 +98,14 @@
   14.79          val cpo_thms' = map (Thm.transfer theory') cpo_thms;
   14.80        in
   14.81          theory'
   14.82 -        |> Sign.add_path name
   14.83 +        |> Sign.add_path (Binding.name_of name)
   14.84          |> PureThy.add_thms
   14.85 -          ([((Binding.name ("adm_" ^ name), admissible'), []),
   14.86 -            ((Binding.name ("cont_" ^ Rep_name), @{thm typedef_cont_Rep} OF cpo_thms'), []),
   14.87 -            ((Binding.name ("cont_" ^ Abs_name), @{thm typedef_cont_Abs} OF cpo_thms'), []),
   14.88 -            ((Binding.name ("lub_" ^ name), @{thm typedef_lub} OF cpo_thms'), []),
   14.89 -            ((Binding.name ("thelub_" ^ name), @{thm typedef_thelub} OF cpo_thms'), []),
   14.90 -            ((Binding.name ("compact_" ^ name), @{thm typedef_compact} OF cpo_thms'), [])])
   14.91 +          ([((Binding.prefix_name "adm_" name, admissible'), []),
   14.92 +            ((Binding.prefix_name "cont_" Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []),
   14.93 +            ((Binding.prefix_name "cont_" Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []),
   14.94 +            ((Binding.prefix_name "lub_" name, @{thm typedef_lub} OF cpo_thms'), []),
   14.95 +            ((Binding.prefix_name "thelub_" name, @{thm typedef_thelub} OF cpo_thms'), []),
   14.96 +            ((Binding.prefix_name "compact_" name, @{thm typedef_compact} OF cpo_thms'), [])])
   14.97          |> snd
   14.98          |> Sign.parent_path
   14.99        end;
  14.100 @@ -117,15 +120,14 @@
  14.101          val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
  14.102        in
  14.103          theory'
  14.104 -        |> Sign.add_path name
  14.105 +        |> Sign.add_path (Binding.name_of name)
  14.106          |> PureThy.add_thms
  14.107 -            ([((Binding.name (Rep_name ^ "_strict"), @{thm typedef_Rep_strict} OF pcpo_thms'), []),
  14.108 -              ((Binding.name (Abs_name ^ "_strict"), @{thm typedef_Abs_strict} OF pcpo_thms'), []),
  14.109 -              ((Binding.name (Rep_name ^ "_strict_iff"), @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
  14.110 -              ((Binding.name (Abs_name ^ "_strict_iff"), @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
  14.111 -              ((Binding.name (Rep_name ^ "_defined"), @{thm typedef_Rep_defined} OF pcpo_thms'), []),
  14.112 -              ((Binding.name (Abs_name ^ "_defined"), @{thm typedef_Abs_defined} OF pcpo_thms'), [])
  14.113 -              ])
  14.114 +          ([((Binding.suffix_name "_strict" Rep_name, @{thm typedef_Rep_strict} OF pcpo_thms'), []),
  14.115 +            ((Binding.suffix_name "_strict" Abs_name, @{thm typedef_Abs_strict} OF pcpo_thms'), []),
  14.116 +            ((Binding.suffix_name "_strict_iff" Rep_name, @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
  14.117 +            ((Binding.suffix_name "_strict_iff" Abs_name, @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
  14.118 +            ((Binding.suffix_name "_defined" Rep_name, @{thm typedef_Rep_defined} OF pcpo_thms'), []),
  14.119 +            ((Binding.suffix_name "_defined" Abs_name, @{thm typedef_Abs_defined} OF pcpo_thms'), [])])
  14.120          |> snd
  14.121          |> Sign.parent_path
  14.122        end;
  14.123 @@ -142,7 +144,8 @@
  14.124      then (goal_UU_mem, goal_admissible, pcpodef_result)
  14.125      else (goal_nonempty, goal_admissible, cpodef_result)
  14.126    end
  14.127 -  handle ERROR msg => err_in_cpodef msg name;
  14.128 +  handle ERROR msg =>
  14.129 +    cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
  14.130  
  14.131  
  14.132  (* proof interface *)
  14.133 @@ -174,14 +177,14 @@
  14.134  
  14.135  val typedef_proof_decl =
  14.136    Scan.optional (P.$$$ "(" |--
  14.137 -      ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
  14.138 +      ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
  14.139          --| P.$$$ ")") (true, NONE) --
  14.140 -    (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
  14.141 -    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
  14.142 +    (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
  14.143 +    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
  14.144  
  14.145  fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
  14.146    (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
  14.147 -    ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
  14.148 +    ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs);
  14.149  
  14.150  val _ =
  14.151    OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
    15.1 --- a/src/ZF/Tools/datatype_package.ML	Sat Mar 07 22:16:50 2009 +0100
    15.2 +++ b/src/ZF/Tools/datatype_package.ML	Sat Mar 07 22:17:25 2009 +0100
    15.3 @@ -245,14 +245,14 @@
    15.4    fun add_recursor thy =
    15.5        if need_recursor then
    15.6             thy |> Sign.add_consts_i
    15.7 -                    [(recursor_base_name, recursor_typ, NoSyn)]
    15.8 +                    [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
    15.9                 |> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
   15.10        else thy;
   15.11  
   15.12    val (con_defs, thy0) = thy_path
   15.13               |> Sign.add_consts_i
   15.14 -                 ((case_base_name, case_typ, NoSyn) ::
   15.15 -                  map #1 (List.concat con_ty_lists))
   15.16 +                 (map (fn (c, T, mx) => (Binding.name c, T, mx))
   15.17 +                  ((case_base_name, case_typ, NoSyn) :: map #1 (List.concat con_ty_lists)))
   15.18               |> PureThy.add_defs false
   15.19                   (map (Thm.no_attributes o apfst Binding.name)
   15.20                    (case_def ::
   15.21 @@ -302,7 +302,7 @@
   15.22  
   15.23    (*** Prove the recursor theorems ***)
   15.24  
   15.25 -  val recursor_eqns = case try (Thm.get_def thy1) recursor_base_name of
   15.26 +  val recursor_eqns = case try (Drule.get_def thy1) recursor_base_name of
   15.27       NONE => (writeln "  [ No recursion operator ]";
   15.28                [])
   15.29     | SOME recursor_def =>
    16.1 --- a/src/ZF/Tools/inductive_package.ML	Sat Mar 07 22:16:50 2009 +0100
    16.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Mar 07 22:17:25 2009 +0100
    16.3 @@ -180,7 +180,7 @@
    16.4  
    16.5    (*fetch fp definitions from the theory*)
    16.6    val big_rec_def::part_rec_defs =
    16.7 -    map (Thm.get_def thy1)
    16.8 +    map (Drule.get_def thy1)
    16.9          (case rec_names of [_] => rec_names
   16.10                           | _   => big_rec_base_name::rec_names);
   16.11  
    17.1 --- a/src/ZF/ind_syntax.ML	Sat Mar 07 22:16:50 2009 +0100
    17.2 +++ b/src/ZF/ind_syntax.ML	Sat Mar 07 22:17:25 2009 +0100
    17.3 @@ -73,7 +73,7 @@
    17.4          val T = (map (#2 o dest_Free) args) ---> iT
    17.5                  handle TERM _ => error
    17.6                      "Bad variable in constructor specification"
    17.7 -        val name = Syntax.const_name id syn  (*handle infix constructors*)
    17.8 +        val name = Syntax.const_name syn id
    17.9      in ((id,T,syn), name, args, prems) end;
   17.10  
   17.11  val read_constructs = map o map o read_construct;