handle Option instead of OPTION;
authorwenzelm
Thu Apr 07 09:24:35 2005 +0200 (2005-04-07 ago)
changeset 15660255055554c67
parent 15659 043c460af14d
child 15661 9ef583b08647
handle Option instead of OPTION;
src/HOL/Tools/inductive_codegen.ML
src/Provers/Arith/fast_lin_arith.ML
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Apr 06 18:13:30 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Apr 07 09:24:35 2005 +0200
     1.3 @@ -229,7 +229,7 @@
     1.4              term_vs t subset vs andalso
     1.5              forall is_eqT dupTs
     1.6            end)
     1.7 -            (modes_of modes t handle OPTION => [Mode (([], []), [])])
     1.8 +            (modes_of modes t handle Option => [Mode (([], []), [])])
     1.9        | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), []))
    1.10            else NONE) ps);
    1.11  
    1.12 @@ -590,7 +590,7 @@
    1.13    end;
    1.14  
    1.15  fun find_mode s u modes is = (case find_first (fn Mode ((_, js), _) => is=js)
    1.16 -  (modes_of modes u handle OPTION => []) of
    1.17 +  (modes_of modes u handle Option => []) of
    1.18       NONE => error ("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
    1.19     | mode => mode);
    1.20  
     2.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Wed Apr 06 18:13:30 2005 +0200
     2.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Apr 07 09:24:35 2005 +0200
     2.3 @@ -439,7 +439,7 @@
     2.4          case add2 thm1 thm2 of
     2.5            NONE => (case try_add ([thm1] RL inj_thms) thm2 of
     2.6                       NONE => ( valOf(try_add ([thm2] RL inj_thms) thm1)
     2.7 -                               handle OPTION =>
     2.8 +                               handle Option =>
     2.9                                 (trace_thm "" thm1; trace_thm "" thm2;
    2.10                                  sys_error "Lin.arith. failed to add thms")
    2.11                               )