delete structure Basic_Record; avoid `record` in names in structure Record
authorhaftmann
Tue Jul 27 17:09:35 2010 +0200 (2010-07-27)
changeset 380123ca193a6ae5a
parent 37974 d9549f9da779
child 38013 0c15b8a655cd
delete structure Basic_Record; avoid `record` in names in structure Record
src/HOL/Hoare/hoare_tac.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Tools/record.ML
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/ex/Records.thy
     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Mon Jul 26 14:44:07 2010 +0200
     1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Tue Jul 27 17:09:35 2010 +0200
     1.3 @@ -125,7 +125,7 @@
     1.4  
     1.5  fun BasicSimpTac var_names tac =
     1.6    simp_tac
     1.7 -    (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [record_simproc])
     1.8 +    (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [Record.simproc])
     1.9    THEN_MAYBE' MaxSimpTac var_names tac;
    1.10  
    1.11  
     2.1 --- a/src/HOL/Statespace/state_fun.ML	Mon Jul 26 14:44:07 2010 +0200
     2.2 +++ b/src/HOL/Statespace/state_fun.ML	Tue Jul 27 17:09:35 2010 +0200
     2.3 @@ -272,7 +272,7 @@
     2.4           val ss' = (Simplifier.context ctxt ex_lookup_ss);
     2.5           fun prove prop =
     2.6             Goal.prove_global thy [] [] prop 
     2.7 -             (fn _ => record_split_simp_tac [] (K ~1) 1 THEN
     2.8 +             (fn _ => Record.split_simp_tac [] (K ~1) 1 THEN
     2.9                        simp_tac ss' 1);
    2.10  
    2.11           fun mkeq (swap,Teq,lT,lo,d,n,x,s) i =
     3.1 --- a/src/HOL/Tools/record.ML	Mon Jul 26 14:44:07 2010 +0200
     3.2 +++ b/src/HOL/Tools/record.ML	Tue Jul 27 17:09:35 2010 +0200
     3.3 @@ -7,9 +7,13 @@
     3.4  Extensible records with structural subtyping.
     3.5  *)
     3.6  
     3.7 -signature BASIC_RECORD =
     3.8 +signature RECORD =
     3.9  sig
    3.10 -  type record_info =
    3.11 +  val print_type_abbr: bool Unsynchronized.ref
    3.12 +  val print_type_as_fields: bool Unsynchronized.ref
    3.13 +  val timing: bool Unsynchronized.ref
    3.14 +
    3.15 +  type info =
    3.16     {args: (string * sort) list,
    3.17      parent: (typ list * string) option,
    3.18      fields: (string * typ) list,
    3.19 @@ -19,30 +23,11 @@
    3.20      fold_congs: thm list, unfold_congs: thm list, splits: thm list, defs: thm list,
    3.21      surjective: thm, equality: thm, induct_scheme: thm, induct: thm, cases_scheme: thm,
    3.22      cases: thm, simps: thm list, iffs: thm list}
    3.23 -  val get_record: theory -> string -> record_info option
    3.24 -  val the_record: theory -> string -> record_info
    3.25 -  val record_simproc: simproc
    3.26 -  val record_eq_simproc: simproc
    3.27 -  val record_upd_simproc: simproc
    3.28 -  val record_split_simproc: (term -> int) -> simproc
    3.29 -  val record_ex_sel_eq_simproc: simproc
    3.30 -  val record_split_tac: int -> tactic
    3.31 -  val record_split_simp_tac: thm list -> (term -> int) -> int -> tactic
    3.32 -  val record_split_name: string
    3.33 -  val record_split_wrapper: string * wrapper
    3.34 -  val print_record_type_abbr: bool Unsynchronized.ref
    3.35 -  val print_record_type_as_fields: bool Unsynchronized.ref
    3.36 -end;
    3.37 -
    3.38 -signature RECORD =
    3.39 -sig
    3.40 -  include BASIC_RECORD
    3.41 -  val timing: bool Unsynchronized.ref
    3.42 -  val updateN: string
    3.43 -  val ext_typeN: string
    3.44 -  val extN: string
    3.45 -  val makeN: string
    3.46 -  val moreN: string
    3.47 +  val get_info: theory -> string -> info option
    3.48 +  val the_info: theory -> string -> info
    3.49 +  val add_record: bool -> (string * sort) list * binding -> (typ list * string) option ->
    3.50 +    (binding * typ * mixfix) list -> theory -> theory
    3.51 +
    3.52    val last_extT: typ -> (string * typ list) option
    3.53    val dest_recTs: typ -> (string * typ list) list
    3.54    val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ)
    3.55 @@ -51,13 +36,20 @@
    3.56    val get_extension: theory -> string -> (string * typ list) option
    3.57    val get_extinjects: theory -> thm list
    3.58    val get_simpset: theory -> simpset
    3.59 -  val print_records: theory -> unit
    3.60 +  val simproc: simproc
    3.61 +  val eq_simproc: simproc
    3.62 +  val upd_simproc: simproc
    3.63 +  val split_simproc: (term -> int) -> simproc
    3.64 +  val ex_sel_eq_simproc: simproc
    3.65 +  val split_tac: int -> tactic
    3.66 +  val split_simp_tac: thm list -> (term -> int) -> int -> tactic
    3.67 +  val split_wrapper: string * wrapper
    3.68 +
    3.69 +  val updateN: string
    3.70 +  val ext_typeN: string
    3.71 +  val extN: string
    3.72    val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list
    3.73    val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list
    3.74 -  val add_record: bool -> (string * sort) list * binding -> (typ list * string) option ->
    3.75 -    (binding * typ * mixfix) list -> theory -> theory
    3.76 -  val add_record_cmd: bool -> (string * string option) list * binding -> string option ->
    3.77 -    (binding * string * mixfix) list -> theory -> theory
    3.78    val setup: theory -> theory
    3.79  end;
    3.80  
    3.81 @@ -339,9 +331,9 @@
    3.82  
    3.83  (** record info **)
    3.84  
    3.85 -(* type record_info and parent_info *)
    3.86 -
    3.87 -type record_info =
    3.88 +(* type info and parent_info *)
    3.89 +
    3.90 +type info =
    3.91   {args: (string * sort) list,
    3.92    parent: (typ list * string) option,
    3.93    fields: (string * typ) list,
    3.94 @@ -372,11 +364,11 @@
    3.95    simps: thm list,
    3.96    iffs: thm list};
    3.97  
    3.98 -fun make_record_info args parent fields extension
    3.99 +fun make_info args parent fields extension
   3.100      ext_induct ext_inject ext_surjective ext_split ext_def
   3.101      select_convs update_convs select_defs update_defs fold_congs unfold_congs splits defs
   3.102      surjective equality induct_scheme induct cases_scheme cases
   3.103 -    simps iffs : record_info =
   3.104 +    simps iffs : info =
   3.105   {args = args, parent = parent, fields = fields, extension = extension,
   3.106    ext_induct = ext_induct, ext_inject = ext_inject, ext_surjective = ext_surjective,
   3.107    ext_split = ext_split, ext_def = ext_def, select_convs = select_convs,
   3.108 @@ -399,8 +391,8 @@
   3.109  
   3.110  (* theory data *)
   3.111  
   3.112 -type record_data =
   3.113 - {records: record_info Symtab.table,
   3.114 +type data =
   3.115 + {records: info Symtab.table,
   3.116    sel_upd:
   3.117     {selectors: (int * bool) Symtab.table,
   3.118      updates: string Symtab.table,
   3.119 @@ -415,17 +407,17 @@
   3.120    extfields: (string * typ) list Symtab.table,  (*maps extension to its fields*)
   3.121    fieldext: (string * typ list) Symtab.table};  (*maps field to its extension*)
   3.122  
   3.123 -fun make_record_data
   3.124 +fun make_data
   3.125      records sel_upd equalities extinjects extsplit splits extfields fieldext =
   3.126   {records = records, sel_upd = sel_upd,
   3.127    equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
   3.128 -  extfields = extfields, fieldext = fieldext }: record_data;
   3.129 +  extfields = extfields, fieldext = fieldext }: data;
   3.130  
   3.131  structure Records_Data = Theory_Data
   3.132  (
   3.133 -  type T = record_data;
   3.134 +  type T = data;
   3.135    val empty =
   3.136 -    make_record_data Symtab.empty
   3.137 +    make_data Symtab.empty
   3.138        {selectors = Symtab.empty, updates = Symtab.empty,
   3.139            simpset = HOL_basic_ss, defset = HOL_basic_ss,
   3.140            foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
   3.141 @@ -454,7 +446,7 @@
   3.142       splits = splits2,
   3.143       extfields = extfields2,
   3.144       fieldext = fieldext2}) =
   3.145 -    make_record_data
   3.146 +    make_data
   3.147        (Symtab.merge (K true) (recs1, recs2))
   3.148        {selectors = Symtab.merge (K true) (sels1, sels2),
   3.149          updates = Symtab.merge (K true) (upds1, upds2),
   3.150 @@ -472,32 +464,13 @@
   3.151        (Symtab.merge (K true) (fieldext1, fieldext2));
   3.152  );
   3.153  
   3.154 -fun print_records thy =
   3.155 -  let
   3.156 -    val {records = recs, ...} = Records_Data.get thy;
   3.157 -    val prt_typ = Syntax.pretty_typ_global thy;
   3.158 -
   3.159 -    fun pretty_parent NONE = []
   3.160 -      | pretty_parent (SOME (Ts, name)) =
   3.161 -          [Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
   3.162 -
   3.163 -    fun pretty_field (c, T) = Pretty.block
   3.164 -      [Pretty.str (Sign.extern_const thy c), Pretty.str " ::",
   3.165 -        Pretty.brk 1, Pretty.quote (prt_typ T)];
   3.166 -
   3.167 -    fun pretty_record (name, {args, parent, fields, ...}: record_info) =
   3.168 -      Pretty.block (Pretty.fbreaks (Pretty.block
   3.169 -        [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
   3.170 -        pretty_parent parent @ map pretty_field fields));
   3.171 -  in map pretty_record (Symtab.dest recs) |> Pretty.chunks |> Pretty.writeln end;
   3.172 -
   3.173  
   3.174  (* access 'records' *)
   3.175  
   3.176 -val get_record = Symtab.lookup o #records o Records_Data.get;
   3.177 -
   3.178 -fun the_record thy name =
   3.179 -  (case get_record thy name of
   3.180 +val get_info = Symtab.lookup o #records o Records_Data.get;
   3.181 +
   3.182 +fun the_info thy name =
   3.183 +  (case get_info thy name of
   3.184      SOME info => info
   3.185    | NONE => error ("Unknown record type " ^ quote name));
   3.186  
   3.187 @@ -505,7 +478,7 @@
   3.188    let
   3.189      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   3.190        Records_Data.get thy;
   3.191 -    val data = make_record_data (Symtab.update (name, info) records)
   3.192 +    val data = make_data (Symtab.update (name, info) records)
   3.193        sel_upd equalities extinjects extsplit splits extfields fieldext;
   3.194    in Records_Data.put data thy end;
   3.195  
   3.196 @@ -538,7 +511,7 @@
   3.197  
   3.198      val {records, sel_upd = {selectors, updates, simpset, defset, foldcong, unfoldcong},
   3.199        equalities, extinjects, extsplit, splits, extfields, fieldext} = Records_Data.get thy;
   3.200 -    val data = make_record_data records
   3.201 +    val data = make_data records
   3.202        {selectors = fold Symtab.update_new sels selectors,
   3.203          updates = fold Symtab.update_new upds updates,
   3.204          simpset = Simplifier.addsimps (simpset, simps),
   3.205 @@ -551,11 +524,11 @@
   3.206  
   3.207  (* access 'equalities' *)
   3.208  
   3.209 -fun add_record_equalities name thm thy =
   3.210 +fun add_equalities name thm thy =
   3.211    let
   3.212      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   3.213        Records_Data.get thy;
   3.214 -    val data = make_record_data records sel_upd
   3.215 +    val data = make_data records sel_upd
   3.216        (Symtab.update_new (name, thm) equalities) extinjects extsplit splits extfields fieldext;
   3.217    in Records_Data.put data thy end;
   3.218  
   3.219 @@ -569,7 +542,7 @@
   3.220      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   3.221        Records_Data.get thy;
   3.222      val data =
   3.223 -      make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
   3.224 +      make_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects)
   3.225          extsplit splits extfields fieldext;
   3.226    in Records_Data.put data thy end;
   3.227  
   3.228 @@ -583,19 +556,19 @@
   3.229      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   3.230        Records_Data.get thy;
   3.231      val data =
   3.232 -      make_record_data records sel_upd equalities extinjects
   3.233 +      make_data records sel_upd equalities extinjects
   3.234          (Symtab.update_new (name, thm) extsplit) splits extfields fieldext;
   3.235    in Records_Data.put data thy end;
   3.236  
   3.237  
   3.238  (* access 'splits' *)
   3.239  
   3.240 -fun add_record_splits name thmP thy =
   3.241 +fun add_splits name thmP thy =
   3.242    let
   3.243      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   3.244        Records_Data.get thy;
   3.245      val data =
   3.246 -      make_record_data records sel_upd equalities extinjects extsplit
   3.247 +      make_data records sel_upd equalities extinjects extsplit
   3.248          (Symtab.update_new (name, thmP) splits) extfields fieldext;
   3.249    in Records_Data.put data thy end;
   3.250  
   3.251 @@ -615,7 +588,7 @@
   3.252      val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields, fieldext} =
   3.253        Records_Data.get thy;
   3.254      val data =
   3.255 -      make_record_data records sel_upd equalities extinjects extsplit splits
   3.256 +      make_data records sel_upd equalities extinjects extsplit splits
   3.257          (Symtab.update_new (name, fields) extfields) fieldext;
   3.258    in Records_Data.put data thy end;
   3.259  
   3.260 @@ -655,7 +628,7 @@
   3.261      val fieldext' =
   3.262        fold (fn field => Symtab.update_new (field, extname_types)) fields fieldext;
   3.263      val data =
   3.264 -      make_record_data records sel_upd equalities extinjects
   3.265 +      make_data records sel_upd equalities extinjects
   3.266          extsplit splits extfields fieldext';
   3.267    in Records_Data.put data thy end;
   3.268  
   3.269 @@ -670,7 +643,7 @@
   3.270          fun err msg = error (msg ^ " parent record " ^ quote name);
   3.271  
   3.272          val {args, parent, fields, extension, induct_scheme, ext_def, ...} =
   3.273 -          (case get_record thy name of SOME info => info | NONE => err "Unknown");
   3.274 +          (case get_info thy name of SOME info => info | NONE => err "Unknown");
   3.275          val _ = if length types <> length args then err "Bad number of arguments for" else ();
   3.276  
   3.277          fun bad_inst ((x, S), T) =
   3.278 @@ -837,8 +810,8 @@
   3.279  
   3.280  (* print translations *)
   3.281  
   3.282 -val print_record_type_abbr = Unsynchronized.ref true;
   3.283 -val print_record_type_as_fields = Unsynchronized.ref true;
   3.284 +val print_type_abbr = Unsynchronized.ref true;
   3.285 +val print_type_as_fields = Unsynchronized.ref true;
   3.286  
   3.287  
   3.288  local
   3.289 @@ -886,7 +859,7 @@
   3.290      val _ = null fields andalso raise Match;
   3.291      val u = foldr1 field_types_tr' (map (field_type_tr' o apsnd term_of_type) fields);
   3.292    in
   3.293 -    if not (! print_record_type_as_fields) orelse null fields then raise Match
   3.294 +    if not (! print_type_as_fields) orelse null fields then raise Match
   3.295      else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
   3.296      else Syntax.const @{syntax_const "_record_type_scheme"} $ u $ term_of_type moreT
   3.297    end;
   3.298 @@ -906,7 +879,7 @@
   3.299  
   3.300      fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
   3.301    in
   3.302 -    if ! print_record_type_abbr then
   3.303 +    if ! print_type_abbr then
   3.304        (case last_extT T of
   3.305          SOME (name, _) =>
   3.306            if name = last_ext then
   3.307 @@ -1175,7 +1148,7 @@
   3.308  
   3.309  in
   3.310  
   3.311 -(* record_simproc *)
   3.312 +(* simproc *)
   3.313  
   3.314  (*
   3.315    Simplify selections of an record update:
   3.316 @@ -1191,7 +1164,7 @@
   3.317    - If X is a more-selector we have to make sure that S is not in the updated
   3.318      subrecord.
   3.319  *)
   3.320 -val record_simproc =
   3.321 +val simproc =
   3.322    Simplifier.simproc @{theory HOL} "record_simp" ["x"]
   3.323      (fn thy => fn _ => fn t =>
   3.324        (case t of
   3.325 @@ -1255,7 +1228,7 @@
   3.326    end;
   3.327  
   3.328  
   3.329 -(* record_upd_simproc *)
   3.330 +(* upd_simproc *)
   3.331  
   3.332  (*Simplify multiple updates:
   3.333      (1) "N_update y (M_update g (N_update x (M_update f r))) =
   3.334 @@ -1265,7 +1238,7 @@
   3.335    In both cases "more" updates complicate matters: for this reason
   3.336    we omit considering further updates if doing so would introduce
   3.337    both a more update and an update to a field within it.*)
   3.338 -val record_upd_simproc =
   3.339 +val upd_simproc =
   3.340    Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"]
   3.341      (fn thy => fn _ => fn t =>
   3.342        let
   3.343 @@ -1363,7 +1336,7 @@
   3.344        in
   3.345          if simp then
   3.346            SOME
   3.347 -            (prove_unfold_defs thy noops' [record_simproc]
   3.348 +            (prove_unfold_defs thy noops' [simproc]
   3.349                (list_all (vars, Logic.mk_equals (lhs, rhs))))
   3.350          else NONE
   3.351        end);
   3.352 @@ -1371,7 +1344,7 @@
   3.353  end;
   3.354  
   3.355  
   3.356 -(* record_eq_simproc *)
   3.357 +(* eq_simproc *)
   3.358  
   3.359  (*Look up the most specific record-equality.
   3.360  
   3.361 @@ -1379,13 +1352,13 @@
   3.362   Testing equality of records boils down to the test of equality of all components.
   3.363   Therefore the complexity is: #components * complexity for single component.
   3.364   Especially if a record has a lot of components it may be better to split up
   3.365 - the record first and do simplification on that (record_split_simp_tac).
   3.366 + the record first and do simplification on that (split_simp_tac).
   3.367   e.g. r(|lots of updates|) = x
   3.368  
   3.369 -             record_eq_simproc          record_split_simp_tac
   3.370 +             eq_simproc          split_simp_tac
   3.371   Complexity: #components * #updates     #updates
   3.372  *)
   3.373 -val record_eq_simproc =
   3.374 +val eq_simproc =
   3.375    Simplifier.simproc @{theory HOL} "record_eq_simp" ["r = s"]
   3.376      (fn thy => fn _ => fn t =>
   3.377        (case t of Const (@{const_name "op ="}, Type (_, [T, _])) $ _ $ _ =>
   3.378 @@ -1398,14 +1371,14 @@
   3.379        | _ => NONE));
   3.380  
   3.381  
   3.382 -(* record_split_simproc *)
   3.383 +(* split_simproc *)
   3.384  
   3.385  (*Split quantified occurrences of records, for which P holds.  P can peek on the
   3.386    subterm starting at the quantified occurrence of the record (including the quantifier):
   3.387      P t = 0: do not split
   3.388      P t = ~1: completely split
   3.389      P t > 0: split up to given bound of record extensions.*)
   3.390 -fun record_split_simproc P =
   3.391 +fun split_simproc P =
   3.392    Simplifier.simproc @{theory HOL} "record_split_simp" ["x"]
   3.393      (fn thy => fn _ => fn t =>
   3.394        (case t of
   3.395 @@ -1427,20 +1400,20 @@
   3.396                              @{const_name all} => all_thm
   3.397                            | @{const_name All} => All_thm RS eq_reflection
   3.398                            | @{const_name Ex} => Ex_thm RS eq_reflection
   3.399 -                          | _ => error "record_split_simproc"))
   3.400 +                          | _ => error "split_simproc"))
   3.401                    else NONE
   3.402                  end)
   3.403            else NONE
   3.404        | _ => NONE));
   3.405  
   3.406 -val record_ex_sel_eq_simproc =
   3.407 -  Simplifier.simproc @{theory HOL} "record_ex_sel_eq_simproc" ["Ex t"]
   3.408 +val ex_sel_eq_simproc =
   3.409 +  Simplifier.simproc @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
   3.410      (fn thy => fn ss => fn t =>
   3.411        let
   3.412          fun prove prop =
   3.413            prove_global true thy [] prop
   3.414              (fn _ => simp_tac (Simplifier.inherit_context ss (get_simpset thy)
   3.415 -                addsimps @{thms simp_thms} addsimprocs [record_split_simproc (K ~1)]) 1);
   3.416 +                addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1);
   3.417  
   3.418          fun mkeq (lr, Teq, (sel, Tsel), x) i =
   3.419            if is_selector thy sel then
   3.420 @@ -1474,7 +1447,7 @@
   3.421        end);
   3.422  
   3.423  
   3.424 -(* record_split_simp_tac *)
   3.425 +(* split_simp_tac *)
   3.426  
   3.427  (*Split (and simplify) all records in the goal for which P holds.
   3.428    For quantified occurrences of a record
   3.429 @@ -1483,7 +1456,7 @@
   3.430    P t = 0: do not split
   3.431    P t = ~1: completely split
   3.432    P t > 0: split up to given bound of record extensions.*)
   3.433 -fun record_split_simp_tac thms P = CSUBGOAL (fn (cgoal, i) =>
   3.434 +fun split_simp_tac thms P = CSUBGOAL (fn (cgoal, i) =>
   3.435    let
   3.436      val thy = Thm.theory_of_cterm cgoal;
   3.437  
   3.438 @@ -1525,7 +1498,7 @@
   3.439                else NONE
   3.440              end));
   3.441  
   3.442 -    val simprocs = if has_rec goal then [record_split_simproc P] else [];
   3.443 +    val simprocs = if has_rec goal then [split_simproc P] else [];
   3.444      val thms' = K_comp_convs @ thms;
   3.445    in
   3.446      EVERY split_frees_tacs THEN
   3.447 @@ -1533,10 +1506,10 @@
   3.448    end);
   3.449  
   3.450  
   3.451 -(* record_split_tac *)
   3.452 +(* split_tac *)
   3.453  
   3.454  (*Split all records in the goal, which are quantified by !! or ALL.*)
   3.455 -val record_split_tac = CSUBGOAL (fn (cgoal, i) =>
   3.456 +val split_tac = CSUBGOAL (fn (cgoal, i) =>
   3.457    let
   3.458      val goal = term_of cgoal;
   3.459  
   3.460 @@ -1550,15 +1523,15 @@
   3.461        | is_all _ = 0;
   3.462    in
   3.463      if has_rec goal then
   3.464 -      Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [record_split_simproc is_all]) i
   3.465 +      Simplifier.full_simp_tac (HOL_basic_ss addsimprocs [split_simproc is_all]) i
   3.466      else no_tac
   3.467    end);
   3.468  
   3.469  
   3.470  (* wrapper *)
   3.471  
   3.472 -val record_split_name = "record_split_tac";
   3.473 -val record_split_wrapper = (record_split_name, fn tac => record_split_tac ORELSE' tac);
   3.474 +val split_name = "record_split_tac";
   3.475 +val split_wrapper = (split_name, fn tac => split_tac ORELSE' tac);
   3.476  
   3.477  
   3.478  
   3.479 @@ -1842,9 +1815,9 @@
   3.480    in Thm.implies_elim thm' thm end;
   3.481  
   3.482  
   3.483 -(* record_definition *)
   3.484 -
   3.485 -fun record_definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
   3.486 +(* definition *)
   3.487 +
   3.488 +fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy =
   3.489    let
   3.490      val prefix = Binding.name_of binding;
   3.491      val name = Sign.full_name thy binding;
   3.492 @@ -2342,7 +2315,7 @@
   3.493             ((Binding.name "iffs", iffs), [iff_add])];
   3.494  
   3.495      val info =
   3.496 -      make_record_info alphas parent fields extension
   3.497 +      make_info alphas parent fields extension
   3.498          ext_induct ext_inject ext_surjective ext_split ext_def
   3.499          sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
   3.500          surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
   3.501 @@ -2351,10 +2324,10 @@
   3.502        thms_thy'
   3.503        |> put_record name info
   3.504        |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')
   3.505 -      |> add_record_equalities extension_id equality'
   3.506 +      |> add_equalities extension_id equality'
   3.507        |> add_extinjects ext_inject
   3.508        |> add_extsplit extension_name ext_split
   3.509 -      |> add_record_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
   3.510 +      |> add_splits extension_id (split_meta', split_object', split_ex', induct_scheme')
   3.511        |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
   3.512        |> add_fieldext (extension_name, snd extension) (names @ [full_moreN])
   3.513        |> Sign.restore_naming thy;
   3.514 @@ -2408,7 +2381,7 @@
   3.515  
   3.516      val name = Sign.full_name thy binding;
   3.517      val err_dup_record =
   3.518 -      if is_none (get_record thy name) then []
   3.519 +      if is_none (get_info thy name) then []
   3.520        else ["Duplicate definition of record " ^ quote name];
   3.521  
   3.522      val spec_frees = fold Term.add_tfreesT (parent_args @ map #2 bfields) [];
   3.523 @@ -2433,7 +2406,7 @@
   3.524        err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
   3.525      val _ = if null errs then () else error (cat_lines errs);
   3.526    in
   3.527 -    thy |> record_definition (params, binding) parent parents bfields
   3.528 +    thy |> definition (params, binding) parent parents bfields
   3.529    end
   3.530    handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of binding));
   3.531  
   3.532 @@ -2456,7 +2429,7 @@
   3.533    Sign.add_trfuns ([], parse_translation, [], []) #>
   3.534    Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #>
   3.535    Simplifier.map_simpset (fn ss =>
   3.536 -    ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]);
   3.537 +    ss addsimprocs [simproc, upd_simproc, eq_simproc]);
   3.538  
   3.539  
   3.540  (* outer syntax *)
   3.541 @@ -2469,6 +2442,3 @@
   3.542      >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z)));
   3.543  
   3.544  end;
   3.545 -
   3.546 -structure Basic_Record: BASIC_RECORD = Record;
   3.547 -open Basic_Record;
     4.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Mon Jul 26 14:44:07 2010 +0200
     4.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Tue Jul 27 17:09:35 2010 +0200
     4.3 @@ -331,7 +331,7 @@
     4.4  (*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
     4.5  ML {*
     4.6  fun record_auto_tac (cs, ss) =
     4.7 -  auto_tac (cs addIs [ext] addSWrapper record_split_wrapper,
     4.8 +  auto_tac (cs addIs [ext] addSWrapper Record.split_wrapper,
     4.9      ss addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
    4.10        @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
    4.11        @{thm o_apply}, @{thm Let_def}])
     5.1 --- a/src/HOL/ex/Records.thy	Mon Jul 26 14:44:07 2010 +0200
     5.2 +++ b/src/HOL/ex/Records.thy	Tue Jul 27 17:09:35 2010 +0200
     5.3 @@ -249,8 +249,8 @@
     5.4  
     5.5  text {* In some cases its convenient to automatically split
     5.6  (quantified) records. For this purpose there is the simproc @{ML [source]
     5.7 -"Record.record_split_simproc"} and the tactic @{ML [source]
     5.8 -"Record.record_split_simp_tac"}.  The simplification procedure
     5.9 +"Record.split_simproc"} and the tactic @{ML [source]
    5.10 +"Record.split_simp_tac"}.  The simplification procedure
    5.11  only splits the records, whereas the tactic also simplifies the
    5.12  resulting goal with the standard record simplification rules. A
    5.13  (generalized) predicate on the record is passed as parameter that
    5.14 @@ -259,51 +259,51 @@
    5.15  the quantifier). The value @{ML "0"} indicates no split, a value
    5.16  greater @{ML "0"} splits up to the given bound of record extension and
    5.17  finally the value @{ML "~1"} completely splits the record.
    5.18 -@{ML [source] "Record.record_split_simp_tac"} additionally takes a list of
    5.19 +@{ML [source] "Record.split_simp_tac"} additionally takes a list of
    5.20  equations for simplification and can also split fixed record variables.
    5.21  
    5.22  *}
    5.23  
    5.24  lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
    5.25    apply (tactic {* simp_tac
    5.26 -          (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
    5.27 +          (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
    5.28    apply simp
    5.29    done
    5.30  
    5.31  lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
    5.32 -  apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
    5.33 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
    5.34    apply simp
    5.35    done
    5.36  
    5.37  lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
    5.38    apply (tactic {* simp_tac
    5.39 -          (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
    5.40 +          (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
    5.41    apply simp
    5.42    done
    5.43  
    5.44  lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
    5.45 -  apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
    5.46 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
    5.47    apply simp
    5.48    done
    5.49  
    5.50  lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
    5.51    apply (tactic {* simp_tac
    5.52 -          (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
    5.53 +          (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
    5.54    apply auto
    5.55    done
    5.56  
    5.57  lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
    5.58 -  apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
    5.59 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
    5.60    apply auto
    5.61    done
    5.62  
    5.63  lemma "P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
    5.64 -  apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
    5.65 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
    5.66    apply auto
    5.67    done
    5.68  
    5.69  lemma fixes r shows "P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
    5.70 -  apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
    5.71 +  apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
    5.72    apply auto
    5.73    done
    5.74  
    5.75 @@ -316,7 +316,7 @@
    5.76      have "\<exists>x. P x"
    5.77        using pre
    5.78        apply -
    5.79 -      apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
    5.80 +      apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
    5.81        apply auto 
    5.82        done
    5.83    }
    5.84 @@ -324,13 +324,13 @@
    5.85  qed
    5.86  
    5.87  text {* The effect of simproc @{ML [source]
    5.88 -"Record.record_ex_sel_eq_simproc"} is illustrated by the
    5.89 +"Record.ex_sel_eq_simproc"} is illustrated by the
    5.90  following lemma.  
    5.91  *}
    5.92  
    5.93  lemma "\<exists>r. xpos r = x"
    5.94    apply (tactic {*simp_tac 
    5.95 -           (HOL_basic_ss addsimprocs [Record.record_ex_sel_eq_simproc]) 1*})
    5.96 +           (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*})
    5.97    done
    5.98  
    5.99