1.1 --- a/src/HOL/Import/hol4rews.ML	Tue Jul 12 23:22:22 2011 +0200
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Wed Jul 13 04:00:32 2011 +0900
     1.3 @@ -160,7 +160,7 @@
     1.4      let
     1.5          val _ = message "Adding HOL4 rewrite"
     1.6          val th1 = th RS @{thm eq_reflection}
     1.7 -                  handle _ => th
     1.8 +                  handle THM _ => th
     1.9          val current_rews = HOL4Rewrites.get thy
    1.10          val new_rews = insert Thm.eq_thm th1 current_rews
    1.11          val updated_thy  = HOL4Rewrites.put new_rews thy
    1.12 @@ -168,7 +168,7 @@
    1.13          (Context.Theory updated_thy,th1)
    1.14      end
    1.15    | add_hol4_rewrite (context, th) = (context,
    1.16 -      (th RS @{thm eq_reflection} handle _ => th)
    1.17 +      (th RS @{thm eq_reflection} handle THM _ => th)
    1.18      );
    1.19  
    1.20  fun ignore_hol4 bthy bthm thy =