diff -r b22e44496dc2 -r 8f9594c31de4 src/HOL/SMT/Tools/smt_monomorph.ML
--- a/src/HOL/SMT/Tools/smt_monomorph.ML	Tue Oct 20 16:13:01 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_monomorph.ML	Wed Oct 21 08:14:38 2009 +0200
@@ -55,7 +55,7 @@
 fun proper_match ps env =
   forall (forall (not o typ_has_tvars o Envir.subst_type env) o snd) ps
 
-val eq_tab = gen_eq_set (op =) o pairself Vartab.dest
+val eq_tab = eq_set (op =) o pairself Vartab.dest
 
 fun specialize thy cs is ((r, ps), ces) (ts, ns) =
   let