src/HOL/simpdata.ML
changeset 6968 7f2977e96a5c
parent 6915 4ab8e31a8421
child 7031 972b5f62f476
     1.1 --- a/src/HOL/simpdata.ML	Sat Jul 10 21:46:15 1999 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Sat Jul 10 21:48:27 1999 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4                      else  cla addSIs [th]
     1.5                | _ => cla addSIs [th],
     1.6         simp addsimps [th])
     1.7 -      handle _ => error ("AddIffs: theorem must be unconditional\n" ^ 
     1.8 +      handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^ 
     1.9                           string_of_thm th);
    1.10  
    1.11    fun delIff ((cla, simp), th) = 
    1.12 @@ -45,7 +45,7 @@
    1.13                      else cla delrules [th]
    1.14                | _ => cla delrules [th],
    1.15         simp delsimps [th])
    1.16 -      handle _ => (warning("DelIffs: ignoring conditional theorem\n" ^ 
    1.17 +      handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ 
    1.18                            string_of_thm th); (cla, simp));
    1.19  
    1.20    fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)