changeset 29269 | 5c25a2012975 |
parent 29125 | d41182a8135c |
child 30304 | d8e4cd2ac2a1 |
--- 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) =>