src/Pure/meta_simplifier.ML
changeset 33037 b22e44496dc2
parent 32797 2e8fae2d998c
child 33038 8f9594c31de4
     1.1 --- a/src/Pure/meta_simplifier.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -864,7 +864,7 @@
     1.4    while the premises are solved.*)
     1.5  
     1.6  fun cond_skel (args as (_, (lhs, rhs))) =
     1.7 -  if Term.add_vars rhs [] subset Term.add_vars lhs [] then uncond_skel args
     1.8 +  if gen_subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args
     1.9    else skel0;
    1.10  
    1.11  (*