src/HOL/Tools/Function/termination.ML
changeset 31971 8c1b845ed105
parent 31775 2b04504fcb69
child 32135 f645b51e8e54
     1.1 --- a/src/HOL/Tools/Function/termination.ML	Thu Jul 09 17:34:59 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/termination.ML	Thu Jul 09 22:01:41 2009 +0200
     1.3 @@ -51,8 +51,8 @@
     1.4  open FundefLib
     1.5  
     1.6  val term2_ord = prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord
     1.7 -structure Term2tab = TableFun(type key = term * term val ord = term2_ord);
     1.8 -structure Term3tab = TableFun(type key = term * (term * term) val ord = prod_ord TermOrd.fast_term_ord term2_ord);
     1.9 +structure Term2tab = Table(type key = term * term val ord = term2_ord);
    1.10 +structure Term3tab = Table(type key = term * (term * term) val ord = prod_ord TermOrd.fast_term_ord term2_ord);
    1.11  
    1.12  (** Analyzing binary trees **)
    1.13