handle THM exn;
authorwenzelm
Sat Jul 10 21:44:26 1999 +0200 (1999-07-10 ago)
changeset 6966cfa87aef9ccd
parent 6965 a766de752996
child 6967 a3c163ed1e04
handle THM exn;
src/FOL/IFOL.ML
src/Provers/simp.ML
     1.1 --- a/src/FOL/IFOL.ML	Sat Jul 10 21:43:27 1999 +0200
     1.2 +++ b/src/FOL/IFOL.ML	Sat Jul 10 21:44:26 1999 +0200
     1.3 @@ -248,7 +248,7 @@
     1.4  (*Apply an equality or definition ONCE.
     1.5    Fails unless the substitution has an effect*)
     1.6  fun stac th = 
     1.7 -  let val th' = th RS meta_eq_to_obj_eq handle _ => th
     1.8 +  let val th' = th RS meta_eq_to_obj_eq handle THM _ => th
     1.9    in  CHANGED_GOAL (rtac (th' RS ssubst))
    1.10    end;
    1.11  
     2.1 --- a/src/Provers/simp.ML	Sat Jul 10 21:43:27 1999 +0200
     2.2 +++ b/src/Provers/simp.ML	Sat Jul 10 21:44:26 1999 +0200
     2.3 @@ -118,14 +118,14 @@
     2.4  
     2.5  fun find_res thms thm =
     2.6      let fun find [] = (prths thms; error"Check Simp_Data")
     2.7 -          | find(th::thms) = thm RS th handle _ => find thms
     2.8 +          | find(th::thms) = thm RS th handle THM _ => find thms
     2.9      in find thms end;
    2.10  
    2.11  val mk_trans = find_res trans_thms;
    2.12  
    2.13  fun mk_trans2 thm =
    2.14  let fun mk[] = error"Check transitivity"
    2.15 -      | mk(t::ts) = (thm RSN (2,t))  handle _  => mk ts
    2.16 +      | mk(t::ts) = (thm RSN (2,t))  handle THM _  => mk ts
    2.17  in mk trans_thms end;
    2.18  
    2.19  (*Applies tactic and returns the first resulting state, FAILS if none!*)