src/HOL/Statespace/DistinctTreeProver.thy
changeset 35408 b48ab741683b
parent 32960 69916a850301
child 38838 62f6ba39b3d4
     1.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Sat Feb 27 22:52:25 2010 +0100
     1.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Sat Feb 27 23:13:01 2010 +0100
     1.3 @@ -645,9 +645,9 @@
     1.4  val const_decls = map (fn i => Syntax.no_syn 
     1.5                                   ("const" ^ string_of_int i,Type ("nat",[]))) nums
     1.6  
     1.7 -val consts = sort TermOrd.fast_term_ord 
     1.8 +val consts = sort Term_Ord.fast_term_ord 
     1.9                (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
    1.10 -val consts' = sort TermOrd.fast_term_ord 
    1.11 +val consts' = sort Term_Ord.fast_term_ord 
    1.12                (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums')
    1.13  
    1.14  val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts