--- a/src/HOL/Import/hol4rews.ML Wed Jul 13 00:43:07 2011 +0900
+++ b/src/HOL/Import/hol4rews.ML Wed Jul 13 11:31:36 2011 +0900
@@ -160,7 +160,7 @@
let
val _ = message "Adding HOL4 rewrite"
val th1 = th RS @{thm eq_reflection}
- handle _ => th
+ handle THM _ => th
val current_rews = HOL4Rewrites.get thy
val new_rews = insert Thm.eq_thm th1 current_rews
val updated_thy = HOL4Rewrites.put new_rews thy
@@ -168,7 +168,7 @@
(Context.Theory updated_thy,th1)
end
| add_hol4_rewrite (context, th) = (context,
- (th RS @{thm eq_reflection} handle _ => th)
+ (th RS @{thm eq_reflection} handle THM _ => th)
);
fun ignore_hol4 bthy bthm thy =