1.1 --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Apr 19 10:42:45 2006 +0200
     1.2 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Apr 19 10:43:09 2006 +0200
     1.3 @@ -138,14 +138,16 @@
     1.4  (*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
     1.5  fun defines thy (thm,(name,n)) gctypes =
     1.6      let val tm = prop_of thm
     1.7 -	fun defs hs =
     1.8 -            let val (rator,args) = strip_comb hs
     1.9 +	fun defs lhs rhs =
    1.10 +            let val (rator,args) = strip_comb lhs
    1.11  		val ct = const_with_typ thy (dest_ConstFree rator)
    1.12 -            in  forall is_Var args andalso uni_mem ct gctypes  end
    1.13 -		handle ConstFree => false
    1.14 +            in  forall is_Var args andalso uni_mem ct gctypes andalso
    1.15 +                term_varnames rhs subset term_varnames lhs
    1.16 +            end
    1.17 +	    handle ConstFree => false
    1.18      in    
    1.19 -	case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ _) => 
    1.20 -		   defs lhs andalso
    1.21 +	case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 
    1.22 +		   defs lhs rhs andalso
    1.23  		   (Output.debug ("Definition found: " ^ name ^ "_" ^ Int.toString n); true)
    1.24  		 | _ => false
    1.25      end