1.1 --- a/src/HOL/Tools/record.ML	Sat Jun 19 09:14:06 2010 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Jun 19 09:50:30 2010 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4  
     1.5  signature ISO_TUPLE_SUPPORT =
     1.6  sig
     1.7 -  val add_iso_tuple_type: bstring * (string * sort) list ->
     1.8 +  val add_iso_tuple_type: binding * (string * sort) list ->
     1.9      typ * typ -> theory -> (term * term) * theory
    1.10    val mk_cons_tuple: term * term -> term
    1.11    val dest_cons_tuple: term -> term * term
    1.12 @@ -80,7 +80,7 @@
    1.13  val iso_tuple_intro = @{thm isomorphic_tuple_intro};
    1.14  val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
    1.15  
    1.16 -val tuple_iso_tuple = (@{const_name tuple_iso_tuple}, @{thm tuple_iso_tuple});
    1.17 +val tuple_iso_tuple = (@{const_name Record.tuple_iso_tuple}, @{thm tuple_iso_tuple});
    1.18  
    1.19  fun named_cterm_instantiate values thm =
    1.20    let
    1.21 @@ -101,9 +101,9 @@
    1.22    fun merge data = Symtab.merge Thm.eq_thm_prop data;   (* FIXME handle Symtab.DUP ?? *)
    1.23  );
    1.24  
    1.25 -fun do_typedef tyco repT alphas thy =
    1.26 +fun do_typedef b repT alphas thy =
    1.27    let
    1.28 -    val (b_constr, b_proj) = pairself Binding.name ("Abs_" ^  tyco, "Rep_" ^  tyco); (*FIXME*)
    1.29 +    val (b_constr, b_proj) = (Binding.prefix_name "make_" b, Binding.prefix_name "dest_" b);
    1.30      fun get_thms thy tyco =
    1.31        let
    1.32          val SOME { vs, constr, typ = repT, proj_inject, proj_constr, ... } =
    1.33 @@ -114,7 +114,7 @@
    1.34        end;
    1.35    in
    1.36      thy
    1.37 -    |> Typecopy.typecopy (Binding.name tyco, alphas) repT b_constr b_proj
    1.38 +    |> Typecopy.typecopy (b, alphas) repT b_constr b_proj
    1.39      |-> (fn (tyco, _) => `(fn thy => get_thms thy tyco))
    1.40    end;
    1.41  
    1.42 @@ -124,21 +124,21 @@
    1.43      val prodT = HOLogic.mk_prodT (leftT, rightT);
    1.44      val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]);
    1.45    in
    1.46 -    Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $
    1.47 +    Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $
    1.48        Const (fst tuple_iso_tuple, isomT) $ left $ right
    1.49    end;
    1.50  
    1.51 -fun dest_cons_tuple (Const (@{const_name iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
    1.52 +fun dest_cons_tuple (Const (@{const_name Record.iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
    1.53    | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
    1.54  
    1.55 -fun add_iso_tuple_type (name, alphas) (leftT, rightT) thy =
    1.56 +fun add_iso_tuple_type (b, alphas) (leftT, rightT) thy =
    1.57    let
    1.58      val repT = HOLogic.mk_prodT (leftT, rightT);
    1.59  
    1.60      val (((rep_inject, abs_inverse), absC, absT), typ_thy) =
    1.61        thy
    1.62 -      |> do_typedef name repT alphas
    1.63 -      ||> Sign.add_path name;
    1.64 +      |> do_typedef b repT alphas
    1.65 +      ||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*)
    1.66  
    1.67      (*construct a type and body for the isomorphism constant by
    1.68        instantiating the theorem to which the definition will be applied*)
    1.69 @@ -146,7 +146,7 @@
    1.70        rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro;
    1.71      val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
    1.72      val isomT = fastype_of body;
    1.73 -    val isom_binding = Binding.name (name ^ isoN);
    1.74 +    val isom_binding = Binding.suffix_name isoN b;
    1.75      val isom_name = Sign.full_name typ_thy isom_binding;
    1.76      val isom = Const (isom_name, isomT);
    1.77  
    1.78 @@ -157,7 +157,7 @@
    1.79          [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
    1.80  
    1.81      val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
    1.82 -    val cons = Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
    1.83 +    val cons = Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
    1.84  
    1.85      val thm_thy =
    1.86        cdef_thy
    1.87 @@ -1654,7 +1654,7 @@
    1.88          val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
    1.89          val ((_, cons), thy') = thy
    1.90            |> Iso_Tuple_Support.add_iso_tuple_type
    1.91 -            (suffix suff base_name, alphas_zeta) (fastype_of left, fastype_of right);
    1.92 +            (Binding.suffix_name suff (Binding.name base_name), alphas_zeta) (fastype_of left, fastype_of right);
    1.93        in
    1.94          (cons $ left $ right, (thy', i + 1))
    1.95        end;
    1.96 @@ -1846,8 +1846,9 @@
    1.97  
    1.98  fun record_definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
    1.99    let
   1.100 +    val prefix = Binding.name_of binding;
   1.101      val name = Sign.full_name thy binding;
   1.102 -    val full = Sign.full_name_path thy (Binding.name_of binding); (* FIXME Binding.qualified (!?) *)
   1.103 +    val full = Sign.full_name_path thy prefix;
   1.104  
   1.105      val bfields = map (fn (x, T, _) => (x, T)) raw_fields;
   1.106      val field_syntax = map #3 raw_fields;
   1.107 @@ -1859,7 +1860,7 @@
   1.108      val parent_fields_len = length parent_fields;
   1.109      val parent_variants =
   1.110        Name.variant_list [moreN, rN, rN ^ "'", wN] (map Long_Name.base_name parent_names);
   1.111 -    val parent_vars = ListPair.map Free (parent_variants, parent_types);
   1.112 +    val parent_vars = map2 (curry Free) parent_variants parent_types;
   1.113      val parent_len = length parents;
   1.114  
   1.115      val fields = map (apfst full) bfields;
   1.116 @@ -1871,7 +1872,7 @@
   1.117      val variants =
   1.118        Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
   1.119          (map (Binding.name_of o fst) bfields);
   1.120 -    val vars = ListPair.map Free (variants, types);
   1.121 +    val vars = map2 (curry Free) variants types;
   1.122      val named_vars = names ~~ vars;
   1.123      val idxms = 0 upto len;
   1.124  
   1.125 @@ -2090,13 +2091,13 @@
   1.126         map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
   1.127  
   1.128      (*updates*)
   1.129 -    fun mk_upd_prop (i, (c, T)) =
   1.130 +    fun mk_upd_prop i (c, T) =
   1.131        let
   1.132          val x' = Free (Name.variant all_variants (Long_Name.base_name c ^ "'"), T --> T);
   1.133          val n = parent_fields_len + i;
   1.134          val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
   1.135        in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
   1.136 -    val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
   1.137 +    val upd_conv_props = map2 mk_upd_prop idxms fields_more;
   1.138  
   1.139      (*induct*)
   1.140      val induct_scheme_prop =