src/HOL/Tools/res_atp.ML

 fun defines thy thm gctypes =
     let val tm = prop_of thm
         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 gctypes ct andalso
-                Term.add_vars rhs [] subset Term.add_vars lhs []
+            in
+              forall is_Var args andalso uni_mem gctypes ct andalso
+                subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
             end
             handle ConstFree => false
     in    
         case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 
                    defs lhs rhs