changeset 38761 | b32975d3db3e |
parent 36960 | 01594f816e3a |
child 38764 | e6a18808873c |
--- 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