# HG changeset patch # User wenzelm # Date 931636107 -7200 # Node ID 7f2977e96a5c2e312a163142912fdfe52ec82e68 # Parent a3c163ed1e04d0cc81787bf359f9d3454708b85d handle THM/TERM exn; diff -r a3c163ed1e04 -r 7f2977e96a5c src/HOL/Arith.ML --- a/src/HOL/Arith.ML Sat Jul 10 21:46:15 1999 +0200 +++ b/src/HOL/Arith.ML Sat Jul 10 21:48:27 1999 +0200 @@ -865,7 +865,7 @@ val not_leD = linorder_not_le RS iffD1; -fun mk_Eq thm = (thm RS Eq_FalseI) handle _ => (thm RS Eq_TrueI); +fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI); val mk_Trueprop = HOLogic.mk_Trueprop; diff -r a3c163ed1e04 -r 7f2977e96a5c src/HOL/HOL.ML --- a/src/HOL/HOL.ML Sat Jul 10 21:46:15 1999 +0200 +++ b/src/HOL/HOL.ML Sat Jul 10 21:48:27 1999 +0200 @@ -372,7 +372,7 @@ (*Apply an equality or definition ONCE. Fails unless the substitution has an effect*) fun stac th = - let val th' = th RS def_imp_eq handle _ => th + let val th' = th RS def_imp_eq handle THM _ => th in CHANGED_GOAL (rtac (th' RS ssubst)) end; diff -r a3c163ed1e04 -r 7f2977e96a5c src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Sat Jul 10 21:46:15 1999 +0200 +++ b/src/HOL/simpdata.ML Sat Jul 10 21:48:27 1999 +0200 @@ -31,7 +31,7 @@ else cla addSIs [th] | _ => cla addSIs [th], simp addsimps [th]) - handle _ => error ("AddIffs: theorem must be unconditional\n" ^ + handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^ string_of_thm th); fun delIff ((cla, simp), th) = @@ -45,7 +45,7 @@ else cla delrules [th] | _ => cla delrules [th], simp delsimps [th]) - handle _ => (warning("DelIffs: ignoring conditional theorem\n" ^ + handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ string_of_thm th); (cla, simp)); fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)