--- a/src/Provers/hypsubst.ML Tue Nov 12 11:36:18 1996 +0100
+++ b/src/Provers/hypsubst.ML Tue Nov 12 11:36:44 1996 +0100
@@ -54,7 +54,7 @@
exception EQ_VAR;
-fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]);
+fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]);
local val odot = ord"."
in