| changeset 31971 | 8c1b845ed105 |
| parent 31120 | fc654c95c29e |
| child 32402 | 5731300da417 |
--- a/src/HOL/Library/positivstellensatz.ML Thu Jul 09 17:34:59 2009 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Thu Jul 09 22:01:41 2009 +0200 @@ -33,7 +33,7 @@ struct type key = Key.key; -structure Tab = TableFun(Key); +structure Tab = Table(Key); type 'a T = 'a Tab.table; val undefined = Tab.empty;