# HG changeset patch
# User schirmer
# Date 1163523330 -3600
# Node ID a12c0bcd9b2a3ee0056edb2e92b07b8a01f18a86
# Parent  3a2ab1dce297a56acd9dc156af6b897db72acd09
Exported some names

diff -r 3a2ab1dce297 -r a12c0bcd9b2a src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Nov 14 15:29:56 2006 +0100
+++ b/src/HOL/Tools/record_package.ML	Tue Nov 14 17:55:30 2006 +0100
@@ -27,7 +27,14 @@
   val quiet_mode: bool ref
   val record_quick_and_dirty_sensitive: bool 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 KN: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))