src/HOL/Statespace/DistinctTreeProver.thy
changeset 29269 5c25a2012975
parent 28819 daca685d7bb7
child 29291 d3cc5398bad5
     1.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Wed Dec 31 00:08:14 2008 +0100
     1.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Wed Dec 31 15:30:10 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4 -(*  Title:      DistinctTreeProver.thy
     1.5 -    ID:         $Id$
     1.6 +(*  Title:      HOL/Statespace/DistinctTreeProver.thy
     1.7      Author:     Norbert Schirmer, TU Muenchen
     1.8  *)
     1.9  
    1.10 @@ -646,9 +645,9 @@
    1.11  val const_decls = map (fn i => Syntax.no_syn 
    1.12                                   ("const" ^ string_of_int i,Type ("nat",[]))) nums
    1.13  
    1.14 -val consts = sort Term.fast_term_ord 
    1.15 +val consts = sort TermOrd.fast_term_ord 
    1.16                (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
    1.17 -val consts' = sort Term.fast_term_ord 
    1.18 +val consts' = sort TermOrd.fast_term_ord 
    1.19                (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums')
    1.20  
    1.21  val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts