# HG changeset patch
# User paulson
# Date 906725134 -7200
# Node ID d176d9d17181f0407cb7b9c1abc193041c7f52a8
# Parent  301a3a4d3dc7915262fa736f14b0e845929fc1b2
uses BasisLibrary for Int.min

diff -r 301a3a4d3dc7 -r d176d9d17181 src/HOL/TLA/hypsubst.ML
--- a/src/HOL/TLA/hypsubst.ML	Fri Sep 25 14:05:13 1998 +0200
+++ b/src/HOL/TLA/hypsubst.ML	Fri Sep 25 14:05:34 1998 +0200
@@ -63,7 +63,9 @@
 fun STATE tacfun st = tacfun st st;
 
 
-local open Data in
+local open Data 
+           BasisLibrary  (*for Int, List, ...*)
+in
 
 exception EQ_VAR;