diff -r d4f3f8f9c0a5 -r 72dab71cb11e src/HOL/Tools/ATP/reduce_axiomsN.ML
--- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Apr 19 10:42:45 2006 +0200
+++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Apr 19 10:43:09 2006 +0200
@@ -138,14 +138,16 @@
 (*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
 fun defines thy (thm,(name,n)) gctypes =
     let val tm = prop_of thm
-	fun defs hs =
-            let val (rator,args) = strip_comb hs
+	fun defs lhs rhs =
+            let val (rator,args) = strip_comb lhs
 		val ct = const_with_typ thy (dest_ConstFree rator)
-            in  forall is_Var args andalso uni_mem ct gctypes  end
-		handle ConstFree => false
+            in  forall is_Var args andalso uni_mem ct gctypes andalso
+                term_varnames rhs subset term_varnames lhs
+            end
+	    handle ConstFree => false
     in    
-	case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ _) => 
-		   defs lhs andalso
+	case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 
+		   defs lhs rhs andalso
 		   (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true)
 		 | _ => false
     end