more binding; avoid arcane Rep and Abs prefixes

--- a/src/HOL/Tools/record.ML	Sat Jun 19 09:14:06 2010 +0200
+++ b/src/HOL/Tools/record.ML	Sat Jun 19 09:50:30 2010 +0200
@@ -64,7 +64,7 @@
 
 signature ISO_TUPLE_SUPPORT =
 sig
-  val add_iso_tuple_type: bstring * (string * sort) list ->
+  val add_iso_tuple_type: binding * (string * sort) list ->
     typ * typ -> theory -> (term * term) * theory
   val mk_cons_tuple: term * term -> term
   val dest_cons_tuple: term -> term * term
@@ -80,7 +80,7 @@
 val iso_tuple_intro = @{thm isomorphic_tuple_intro};
 val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros};
 
-val tuple_iso_tuple = (@{const_name tuple_iso_tuple}, @{thm tuple_iso_tuple});
+val tuple_iso_tuple = (@{const_name Record.tuple_iso_tuple}, @{thm tuple_iso_tuple});
 
 fun named_cterm_instantiate values thm =
   let
@@ -101,9 +101,9 @@
   fun merge data = Symtab.merge Thm.eq_thm_prop data;   (* FIXME handle Symtab.DUP ?? *)
 );
 
-fun do_typedef tyco repT alphas thy =
+fun do_typedef b repT alphas thy =
   let
-    val (b_constr, b_proj) = pairself Binding.name ("Abs_" ^  tyco, "Rep_" ^  tyco); (*FIXME*)
+    val (b_constr, b_proj) = (Binding.prefix_name "make_" b, Binding.prefix_name "dest_" b);
     fun get_thms thy tyco =
       let
         val SOME { vs, constr, typ = repT, proj_inject, proj_constr, ... } =
@@ -114,7 +114,7 @@
       end;
   in
     thy
-    |> Typecopy.typecopy (Binding.name tyco, alphas) repT b_constr b_proj
+    |> Typecopy.typecopy (b, alphas) repT b_constr b_proj
     |-> (fn (tyco, _) => `(fn thy => get_thms thy tyco))
   end;
 
@@ -124,21 +124,21 @@
     val prodT = HOLogic.mk_prodT (leftT, rightT);
     val isomT = Type (@{type_name tuple_isomorphism}, [prodT, leftT, rightT]);
   in
-    Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $
+    Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> prodT) $
       Const (fst tuple_iso_tuple, isomT) $ left $ right
   end;
 
-fun dest_cons_tuple (Const (@{const_name iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
+fun dest_cons_tuple (Const (@{const_name Record.iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
   | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
 
-fun add_iso_tuple_type (name, alphas) (leftT, rightT) thy =
+fun add_iso_tuple_type (b, alphas) (leftT, rightT) thy =
   let
     val repT = HOLogic.mk_prodT (leftT, rightT);
 
     val (((rep_inject, abs_inverse), absC, absT), typ_thy) =
       thy
-      |> do_typedef name repT alphas
-      ||> Sign.add_path name;
+      |> do_typedef b repT alphas
+      ||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*)
 
     (*construct a type and body for the isomorphism constant by
       instantiating the theorem to which the definition will be applied*)
@@ -146,7 +146,7 @@
       rep_inject RS named_cterm_instantiate [("abst", cterm_of typ_thy absC)] iso_tuple_intro;
     val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst));
     val isomT = fastype_of body;
-    val isom_binding = Binding.name (name ^ isoN);
+    val isom_binding = Binding.suffix_name isoN b;
     val isom_name = Sign.full_name typ_thy isom_binding;
     val isom = Const (isom_name, isomT);
 
@@ -157,7 +157,7 @@
         [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
 
     val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
-    val cons = Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
+    val cons = Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
 
     val thm_thy =
       cdef_thy
@@ -1654,7 +1654,7 @@
         val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
         val ((_, cons), thy') = thy
           |> Iso_Tuple_Support.add_iso_tuple_type
-            (suffix suff base_name, alphas_zeta) (fastype_of left, fastype_of right);
+            (Binding.suffix_name suff (Binding.name base_name), alphas_zeta) (fastype_of left, fastype_of right);
       in
         (cons $ left $ right, (thy', i + 1))
       end;
@@ -1846,8 +1846,9 @@
 
 fun record_definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
   let
+    val prefix = Binding.name_of binding;
     val name = Sign.full_name thy binding;
-    val full = Sign.full_name_path thy (Binding.name_of binding); (* FIXME Binding.qualified (!?) *)
+    val full = Sign.full_name_path thy prefix;
 
     val bfields = map (fn (x, T, _) => (x, T)) raw_fields;
     val field_syntax = map #3 raw_fields;
@@ -1859,7 +1860,7 @@
     val parent_fields_len = length parent_fields;
     val parent_variants =
       Name.variant_list [moreN, rN, rN ^ "'", wN] (map Long_Name.base_name parent_names);
-    val parent_vars = ListPair.map Free (parent_variants, parent_types);
+    val parent_vars = map2 (curry Free) parent_variants parent_types;
     val parent_len = length parents;
 
     val fields = map (apfst full) bfields;
@@ -1871,7 +1872,7 @@
     val variants =
       Name.variant_list (moreN :: rN :: (rN ^ "'") :: wN :: parent_variants)
         (map (Binding.name_of o fst) bfields);
-    val vars = ListPair.map Free (variants, types);
+    val vars = map2 (curry Free) variants types;
     val named_vars = names ~~ vars;
     val idxms = 0 upto len;
 
@@ -2090,13 +2091,13 @@
        map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
 
     (*updates*)
-    fun mk_upd_prop (i, (c, T)) =
+    fun mk_upd_prop i (c, T) =
       let
         val x' = Free (Name.variant all_variants (Long_Name.base_name c ^ "'"), T --> T);
         val n = parent_fields_len + i;
         val args' = nth_map n (K (x' $ nth all_vars_more n)) all_vars_more;
       in mk_upd updateN c x' r_rec0 === mk_rec args' 0 end;
-    val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
+    val upd_conv_props = map2 mk_upd_prop idxms fields_more;
 
     (*induct*)
     val induct_scheme_prop =