diff -r da82b545d2de -r b4d0b545df01 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Tue Jul 11 12:16:58 2006 +0200
+++ b/src/Provers/hypsubst.ML	Tue Jul 11 12:16:59 2006 +0200
@@ -74,7 +74,7 @@
   change it back (any Bound variable will do)*)
 fun contract t =
   (case Pattern.eta_contract_atom t of
-    Free (a, T) => if Term.is_bound a then Bound 0 else Free (a, T)
+    Free (a, T) => if Name.is_bound a then Bound 0 else Free (a, T)
   | t' => t');
 
 fun has_vars t = maxidx_of_term t <> ~1;