1.1 --- a/src/HOL/Tools/Function/function_common.ML	Thu Aug 26 16:56:45 2010 +0200
     1.2 +++ b/src/HOL/Tools/Function/function_common.ML	Thu Aug 26 17:01:12 2010 +0200
     1.3 @@ -175,7 +175,7 @@
     1.4    type T = Proof.context -> tactic
     1.5    val empty = (fn _ => error "Termination prover not configured")
     1.6    val extend = I
     1.7 -  fun merge (a, b) = b  (* FIXME ? *)
     1.8 +  fun merge (a, _) = a
     1.9  )
    1.10  
    1.11  val set_termination_prover = TerminationProver.put

     2.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Aug 26 16:56:45 2010 +0200
     2.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Aug 26 17:01:12 2010 +0200
     2.3 @@ -68,7 +68,7 @@
     2.4    type T = multiset_setup option
     2.5    val empty = NONE
     2.6    val extend = I;
     2.7 -  fun merge (v1, v2) = if is_some v2 then v2 else v1   (* FIXME prefer v1 !?! *)
     2.8 +  fun merge (v1, v2) = if is_some v1 then v1 else v2
     2.9  )
    2.10  
    2.11  val multiset_setup = Multiset_Setup.put o SOME

     3.1 --- a/src/Pure/Proof/extraction.ML	Thu Aug 26 16:56:45 2010 +0200
     3.2 +++ b/src/Pure/Proof/extraction.ML	Thu Aug 26 17:01:12 2010 +0200
     3.3 @@ -204,7 +204,7 @@
     3.4       realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
     3.5       defs = Library.merge Thm.eq_thm (defs1, defs2),
     3.6       expand = Library.merge (op =) (expand1, expand2),
     3.7 -     prep = (case prep1 of NONE => prep2 | _ => prep1)};
     3.8 +     prep = if is_some prep1 then prep1 else prep2};
     3.9  );
    3.10  
    3.11  fun read_condeq thy =