# HG changeset patch # User wenzelm # Date 953985126 -3600 # Node ID bed3b994ab265e44b8013531667125bfc793fc2a # Parent fc22f59f5ae7520dc62c460af27d78fc6ef3dd16 export updateN; diff -r fc22f59f5ae7 -r bed3b994ab26 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Fri Mar 24 21:15:56 2000 +0100 +++ b/src/HOL/Tools/record_package.ML Sat Mar 25 12:52:06 2000 +0100 @@ -17,6 +17,7 @@ sig include BASIC_RECORD_PACKAGE val quiet_mode: bool ref + val updateN: string val moreS: sort val mk_fieldT: (string * typ) * typ -> typ val dest_fieldT: typ -> (string * typ) * typ