handle THM exn;
authorwenzelm
Sat Jul 10 21:50:49 1999 +0200 (1999-07-10)
changeset 6969441393b452c7
parent 6968 7f2977e96a5c
child 6970 ac37a8fcaad1
handle THM exn;
src/FOLP/simp.ML
     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!*)