# HG changeset patch
# User wenzelm
# Date 1294674328 -3600
# Node ID f05976d691419e05b92099f5b4449a59f76fb3fd
# Parent  7a4138cb46dbbede25b4fd889c1866155f43247f
added merge_options convenience;

diff -r 7a4138cb46db -r f05976d69141 src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Mon Jan 10 16:07:16 2011 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Mon Jan 10 16:45:28 2011 +0100
@@ -68,7 +68,7 @@
   type T = multiset_setup option
   val empty = NONE
   val extend = I;
-  fun merge (v1, v2) = if is_some v1 then v1 else v2
+  val merge = merge_options
 )
 
 val multiset_setup = Multiset_Setup.put o SOME
diff -r 7a4138cb46db -r f05976d69141 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Mon Jan 10 16:07:16 2011 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Jan 10 16:45:28 2011 +0100
@@ -138,7 +138,7 @@
      lessD = Thm.merge_thms (lessD1, lessD2),
      neqE = Thm.merge_thms (neqE1, neqE2),
      simpset = Simplifier.merge_ss (simpset1, simpset2),
-     number_of = if is_some number_of1 then number_of1 else number_of2};
+     number_of = merge_options (number_of1, number_of2)};
 );
 
 val map_data = Data.map;
diff -r 7a4138cb46db -r f05976d69141 src/Pure/General/basics.ML
--- a/src/Pure/General/basics.ML	Mon Jan 10 16:07:16 2011 +0100
+++ b/src/Pure/General/basics.ML	Mon Jan 10 16:45:28 2011 +0100
@@ -31,6 +31,7 @@
   val the_list: 'a option -> 'a list
   val the_default: 'a -> 'a option -> 'a
   val perhaps: ('a -> 'a option) -> 'a -> 'a
+  val merge_options: 'a option * 'a option -> 'a option
 
   (*partiality*)
   val try: ('a -> 'b) -> 'a -> 'b option
@@ -90,6 +91,8 @@
 
 fun perhaps f x = the_default x (f x);
 
+fun merge_options (x, y) = if is_some x then x else y;
+
 
 (* partiality *)
 
diff -r 7a4138cb46db -r f05976d69141 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Jan 10 16:07:16 2011 +0100
+++ b/src/Pure/Isar/code.ML	Mon Jan 10 16:45:28 2011 +0100
@@ -1245,7 +1245,7 @@
   type T = (string -> thm -> theory -> theory) option;
   val empty = NONE;
   val extend = I;
-  fun merge (f1, f2) = if is_some f1 then f1 else f2;
+  val merge = merge_options;
 );
 
 fun set_code_target_attr f = Code_Target_Attr.map (K (SOME f));
diff -r 7a4138cb46db -r f05976d69141 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Mon Jan 10 16:07:16 2011 +0100
+++ b/src/Pure/Isar/object_logic.ML	Mon Jan 10 16:45:28 2011 +0100
@@ -54,7 +54,7 @@
 
   fun merge_opt eq (SOME x, SOME y) =
         if eq (x, y) then SOME x else error "Attempt to merge different object-logics"
-    | merge_opt _ (x, y) = if is_some x then x else y;
+    | merge_opt _ data = merge_options data;
 
   fun merge
      (Data {base_sort = base_sort1, judgment = judgment1, atomize_rulify = (atomize1, rulify1)},