diff -r 6aefc5ff8e63 -r 5c25a2012975 src/HOL/Tools/function_package/decompose.ML
--- a/src/HOL/Tools/function_package/decompose.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Tools/function_package/decompose.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -19,7 +19,7 @@
 structure Decompose : DECOMPOSE =
 struct
 
-structure TermGraph = GraphFun(type key = term val ord = Term.fast_term_ord);
+structure TermGraph = GraphFun(type key = term val ord = TermOrd.fast_term_ord);
 
 
 fun derive_chains ctxt chain_tac cont D = Termination.CALLS (fn (cs, i) =>