| changeset 35267 | 8dfd816713c6 |
| parent 35064 | 1bdef0c013d3 |
| child 35756 | cfde251d03a5 |
--- a/src/HOL/Tools/Function/size.ML Fri Feb 19 14:47:00 2010 +0100 +++ b/src/HOL/Tools/Function/size.ML Fri Feb 19 14:47:01 2010 +0100 @@ -25,7 +25,7 @@ val lookup_size = SizeData.get #> Symtab.lookup; -fun plus (t1, t2) = Const (@{const_name Algebras.plus}, +fun plus (t1, t2) = Const (@{const_name Groups.plus}, HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2; fun size_of_type f g h (T as Type (s, Ts)) =