# HG changeset patch
# User wenzelm
# Date 1255796087 -7200
# Node ID 12d830f131acb6e39a3ddc4f22330068ea12fa73
# Parent  45ba8b02e1e41c4a3e389c73fa9481d705a32fe0
removed unused names;

diff -r 45ba8b02e1e4 -r 12d830f131ac src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Oct 17 18:01:24 2009 +0200
+++ b/src/HOL/Tools/record.ML	Sat Oct 17 18:14:47 2009 +0200
@@ -28,12 +28,10 @@
   val timing: bool Unsynchronized.ref
   val record_quick_and_dirty_sensitive: bool Unsynchronized.ref
   val updateN: string
-  val updN: string
   val ext_typeN: string
   val extN: string
   val makeN: string
   val moreN: string
-  val ext_dest: string
   val last_extT: typ -> (string * typ list) option
   val dest_recTs: typ -> (string * typ list) list
   val get_extT_fields: theory -> typ -> (string * typ) list * (string * typ)
@@ -231,9 +229,7 @@
 val ext_typeN = "_ext_type";
 val inner_typeN = "_inner_type";
 val extN ="_ext";
-val ext_dest = "_sel";
 val updateN = "_update";
-val updN = "_upd";
 val makeN = "make";
 val fields_selN = "fields";
 val extendN = "extend";