--- 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))