removed unused names;
authorwenzelm
Sat Oct 17 18:14:47 2009 +0200 (2009-10-17)
changeset 3297312d830f131ac
parent 32972 45ba8b02e1e4
child 32974 2a1aaa2d9e64
removed unused names;
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Tools/record.ML	Sat Oct 17 18:01:24 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Oct 17 18:14:47 2009 +0200
     1.3 @@ -28,12 +28,10 @@
     1.4    val timing: bool Unsynchronized.ref
     1.5    val record_quick_and_dirty_sensitive: bool Unsynchronized.ref
     1.6    val updateN: string
     1.7 -  val updN: string
     1.8    val ext_typeN: string
     1.9    val extN: string
    1.10    val makeN: string
    1.11    val moreN: string
    1.12 -  val ext_dest: string
    1.13    val last_extT: typ -> (string * typ list) option
    1.14    val dest_recTs: typ -> (string * typ list) list
    1.15    val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ)
    1.16 @@ -231,9 +229,7 @@
    1.17  val ext_typeN = "_ext_type";
    1.18  val inner_typeN = "_inner_type";
    1.19  val extN ="_ext";
    1.20 -val ext_dest = "_sel";
    1.21  val updateN = "_update";
    1.22 -val updN = "_upd";
    1.23  val makeN = "make";
    1.24  val fields_selN = "fields";
    1.25  val extendN = "extend";