changeset 31971 | 8c1b845ed105 |
parent 30528 | 7173bf123335 |
child 32432 | 64f30bdd3ba1 |
--- a/src/HOL/Import/hol4rews.ML Thu Jul 09 17:34:59 2009 +0200 +++ b/src/HOL/Import/hol4rews.ML Thu Jul 09 22:01:41 2009 +0200 @@ -1,9 +1,8 @@ (* Title: HOL/Import/hol4rews.ML - ID: $Id$ Author: Sebastian Skalberg (TU Muenchen) *) -structure StringPair = TableFun(type key = string * string val ord = prod_ord string_ord string_ord); +structure StringPair = Table(type key = string * string val ord = prod_ord string_ord string_ord); type holthm = (term * term) list * thm