--- a/src/HOL/Statespace/DistinctTreeProver.thy Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Sat Feb 27 23:13:01 2010 +0100
@@ -645,9 +645,9 @@
val const_decls = map (fn i => Syntax.no_syn
("const" ^ string_of_int i,Type ("nat",[]))) nums
-val consts = sort TermOrd.fast_term_ord
+val consts = sort Term_Ord.fast_term_ord
(map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
-val consts' = sort TermOrd.fast_term_ord
+val consts' = sort Term_Ord.fast_term_ord
(map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums')
val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts