# HG changeset patch
# User paulson
# Date 847795004 -3600
# Node ID 0829b7b632c51b977982fb5f2a37692746433001
# Parent  08c68550460b0132ee1d8bbfe930979e78aee609
Removed a call to polymorphic mem

diff -r 08c68550460b -r 0829b7b632c5 src/Provers/hypsubst.ML
--- 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