# HG changeset patch
# User wenzelm
# Date 1112858675 -7200
# Node ID 255055554c6750b8fe22ad65f5df4a006b10bb46
# Parent  043c460af14db14aa3e6a65aa6a7891fa945a461
handle Option instead of OPTION;

diff -r 043c460af14d -r 255055554c67 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Wed Apr 06 18:13:30 2005 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Apr 07 09:24:35 2005 +0200
@@ -229,7 +229,7 @@
             term_vs t subset vs andalso
             forall is_eqT dupTs
           end)
-            (modes_of modes t handle OPTION => [Mode (([], []), [])])
+            (modes_of modes t handle Option => [Mode (([], []), [])])
       | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), []))
           else NONE) ps);
 
@@ -590,7 +590,7 @@
   end;
 
 fun find_mode s u modes is = (case find_first (fn Mode ((_, js), _) => is=js)
-  (modes_of modes u handle OPTION => []) of
+  (modes_of modes u handle Option => []) of
      NONE => error ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
    | mode => mode);
 
diff -r 043c460af14d -r 255055554c67 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Apr 06 18:13:30 2005 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Apr 07 09:24:35 2005 +0200
@@ -439,7 +439,7 @@
         case add2 thm1 thm2 of
           NONE => (case try_add ([thm1] RL inj_thms) thm2 of
                      NONE => ( valOf(try_add ([thm2] RL inj_thms) thm1)
-                               handle OPTION =>
+                               handle Option =>
                                (trace_thm "" thm1; trace_thm "" thm2;
                                 sys_error "Lin.arith. failed to add thms")
                              )