--- a/src/HOL/Statespace/DistinctTreeProver.thy Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Wed Dec 31 15:30:10 2008 +0100
@@ -1,5 +1,4 @@
-(* Title: DistinctTreeProver.thy
- ID: $Id$
+(* Title: HOL/Statespace/DistinctTreeProver.thy
Author: Norbert Schirmer, TU Muenchen
*)
@@ -646,9 +645,9 @@
val const_decls = map (fn i => Syntax.no_syn
("const" ^ string_of_int i,Type ("nat",[]))) nums
-val consts = sort Term.fast_term_ord
+val consts = sort TermOrd.fast_term_ord
(map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
-val consts' = sort Term.fast_term_ord
+val consts' = sort TermOrd.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