diff -r 5dadc93ff3df -r 94242fa87638 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Fri Mar 07 12:35:06 2014 +0000
+++ b/src/HOL/Tools/Function/termination.ML	Fri Mar 07 14:21:15 2014 +0100
@@ -6,7 +6,6 @@
 
 signature TERMINATION =
 sig
-
   type data
   datatype cell = Less of thm | LessEq of thm * thm | None of thm * thm | False of thm
 
@@ -122,7 +121,7 @@
 (* Build case expression *)
 fun mk_sumcases (sk, _, _, _, _) T fs =
   mk_tree (fn i => (nth fs i, domain_type (fastype_of (nth fs i))))
-          (fn ((f, fT), (g, gT)) => (SumTree.mk_sumcase fT gT T f g, SumTree.mk_sumT fT gT))
+          (fn ((f, fT), (g, gT)) => (Sum_Tree.mk_sumcase fT gT T f g, Sum_Tree.mk_sumT fT gT))
           sk
   |> fst