--- a/src/HOL/Tools/Function/termination.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/HOL/Tools/Function/termination.ML Thu Jul 09 22:01:41 2009 +0200
@@ -51,8 +51,8 @@
open FundefLib
val term2_ord = prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord
-structure Term2tab = TableFun(type key = term * term val ord = term2_ord);
-structure Term3tab = TableFun(type key = term * (term * term) val ord = prod_ord TermOrd.fast_term_ord term2_ord);
+structure Term2tab = Table(type key = term * term val ord = term2_ord);
+structure Term3tab = Table(type key = term * (term * term) val ord = prod_ord TermOrd.fast_term_ord term2_ord);
(** Analyzing binary trees **)