# HG changeset patch
# User wenzelm
# Date 1282834872 -7200
# Node ID b32975d3db3e27d5876c1973d9951b02eadcb52b
# Parent  6f285436e3d6d714ff42bfeb878562253265ca52
theory data merge: prefer left side uniformly;

diff -r 6f285436e3d6 -r b32975d3db3e src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Thu Aug 26 16:56:45 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Thu Aug 26 17:01:12 2010 +0200
@@ -175,7 +175,7 @@
   type T = Proof.context -> tactic
   val empty = (fn _ => error "Termination prover not configured")
   val extend = I
-  fun merge (a, b) = b  (* FIXME ? *)
+  fun merge (a, _) = a
 )
 
 val set_termination_prover = TerminationProver.put
diff -r 6f285436e3d6 -r b32975d3db3e src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Aug 26 16:56:45 2010 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Aug 26 17:01:12 2010 +0200
@@ -68,7 +68,7 @@
   type T = multiset_setup option
   val empty = NONE
   val extend = I;
-  fun merge (v1, v2) = if is_some v2 then v2 else v1   (* FIXME prefer v1 !?! *)
+  fun merge (v1, v2) = if is_some v1 then v1 else v2
 )
 
 val multiset_setup = Multiset_Setup.put o SOME
diff -r 6f285436e3d6 -r b32975d3db3e src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Thu Aug 26 16:56:45 2010 +0200
+++ b/src/Pure/Proof/extraction.ML	Thu Aug 26 17:01:12 2010 +0200
@@ -204,7 +204,7 @@
      realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
      defs = Library.merge Thm.eq_thm (defs1, defs2),
      expand = Library.merge (op =) (expand1, expand2),
-     prep = (case prep1 of NONE => prep2 | _ => prep1)};
+     prep = if is_some prep1 then prep1 else prep2};
 );
 
 fun read_condeq thy =