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