src/FOLP/simp.ML
changeset 6969 441393b452c7
parent 5963 94709c11601e
child 7645 c67115c0e105
     1.1 --- a/src/FOLP/simp.ML	Sat Jul 10 21:48:27 1999 +0200
     1.2 +++ b/src/FOLP/simp.ML	Sat Jul 10 21:50:49 1999 +0200
     1.3 @@ -124,14 +124,14 @@
     1.4  
     1.5  fun find_res thms thm =
     1.6      let fun find [] = (prths thms; error"Check Simp_Data")
     1.7 -          | find(th::thms) = thm RS th handle _ => find thms
     1.8 +          | find(th::thms) = thm RS th handle THM _ => find thms
     1.9      in find thms end;
    1.10  
    1.11  val mk_trans = find_res trans_thms;
    1.12  
    1.13  fun mk_trans2 thm =
    1.14  let fun mk[] = error"Check transitivity"
    1.15 -      | mk(t::ts) = (thm RSN (2,t))  handle _  => mk ts
    1.16 +      | mk(t::ts) = (thm RSN (2,t))  handle THM _  => mk ts
    1.17  in mk trans_thms end;
    1.18  
    1.19  (*Applies tactic and returns the first resulting state, FAILS if none!*)