# HG changeset patch
# User wenzelm
# Date 1223057444 -7200
# Node ID 13e637e0c8762f900a22bb977bfa0b24409dc9b1
# Parent  873726bdfd47b399f73ae14b3a7d4a61255ab305
do not handle Error (which matches arbitrary exceptions!), but ERROR _;

diff -r 873726bdfd47 -r 13e637e0c876 src/HOL/Tools/atp_manager.ML
--- a/src/HOL/Tools/atp_manager.ML	Fri Oct 03 20:10:43 2008 +0200
+++ b/src/HOL/Tools/atp_manager.ML	Fri Oct 03 20:10:44 2008 +0200
@@ -203,7 +203,7 @@
          pgiptype = PgipTypes.Pgipstring,
          get = fn () => !atps,
          set = set_atps}
-        handle Error => warning "Preference already exists";
+        handle ERROR _ => warning "Preference already exists";
 
     val _ = ProofGeneralPgip.add_preference "Proof"
         {name = "ATP - Maximum number",
@@ -212,7 +212,7 @@
          pgiptype = PgipTypes.Pgipstring,
          get = fn () => Int.toString (! maximum_atps),
          set = fn str => set_max_atp (the_default 1 (Int.fromString str))}
-        handle Error => warning "Preference already exists";
+        handle ERROR _ => warning "Preference already exists";
 
     val _ = ProofGeneralPgip.add_preference "Proof"
         {name = "ATP - Timeout",
@@ -221,7 +221,7 @@
          pgiptype = PgipTypes.Pgipstring,
          get = fn () => Int.toString (! timeout),
          set = fn str => set_timeout (the_default 60 (Int.fromString str))}
-        handle Error => warning "Preference already exists";
+        handle ERROR _ => warning "Preference already exists";
 
 
   (* named provers *)