src/HOL/Tools/res_atp.ML
changeset 33037 b22e44496dc2
parent 32994 ccc07fbbfefd
child 33038 8f9594c31de4
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -213,8 +213,9 @@
     1.4          fun defs lhs rhs =
     1.5              let val (rator,args) = strip_comb lhs
     1.6                  val ct = const_with_typ thy (dest_ConstFree rator)
     1.7 -            in  forall is_Var args andalso uni_mem gctypes ct andalso
     1.8 -                Term.add_vars rhs [] subset Term.add_vars lhs []
     1.9 +            in
    1.10 +              forall is_Var args andalso uni_mem gctypes ct andalso
    1.11 +                gen_subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
    1.12              end
    1.13              handle ConstFree => false
    1.14      in