src/FOLP/simp.ML
changeset 33040 cffdb7b28498
parent 32957 675c0c7e6a37
child 33063 4d462963a7db
     1.1 --- a/src/FOLP/simp.ML	Wed Oct 21 08:16:25 2009 +0200
     1.2 +++ b/src/FOLP/simp.ML	Wed Oct 21 10:15:31 2009 +0200
     1.3 @@ -543,7 +543,7 @@
     1.4  fun find_subst sg T =
     1.5  let fun find (thm::thms) =
     1.6          let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
     1.7 -            val [P] = OldTerm.add_term_vars(concl_of thm,[]) \\ [va,vb]
     1.8 +            val [P] = subtract (op =) [va, vb] (OldTerm.add_term_vars (concl_of thm, []));
     1.9              val eqT::_ = binder_types cT
    1.10          in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P)
    1.11             else find thms