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