src/HOL/Tools/Function/context_tree.ML

--- a/src/HOL/Tools/Function/context_tree.ML	Mon Dec 13 10:15:26 2010 +0100
+++ b/src/HOL/Tools/Function/context_tree.ML	Mon Dec 13 10:15:27 2010 +0100
@@ -103,7 +103,7 @@
 (* Called on the INSTANTIATED branches of the congruence rule *)
 fun mk_branch ctx t =
   let
-    val (ctx', fixes, impl) = dest_all_all_ctx ctx t
+    val ((fixes, impl), ctx') = Function_Lib.focus_term t ctx
     val (assms, concl) = Logic.strip_horn impl
   in
     (ctx', fixes, assms, rhs_of concl)