# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1310497232 -32400
# Node ID a72661ba72390816e0233d32a86bc2e9142400ad
# Parent  9bd8d4addd6e29dd056a711740935deb6ae809cd# Parent  a9242e34d71189aa858e0e1d434696ab9e92082c
merge

diff -r 9bd8d4addd6e -r a72661ba7239 src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Tue Jul 12 23:22:22 2011 +0200
+++ b/src/HOL/Import/hol4rews.ML	Wed Jul 13 04:00:32 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 =