added merge_options convenience;

--- 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

--- 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;

--- 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 *)
 

--- 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));

--- 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)},