| changeset 34974 | 18b41bba42b5 |
| parent 33968 | f94fb13ecbb3 |
| child 35021 | c839a4c670c6 |
--- a/src/HOL/Tools/Function/size.ML Thu Jan 28 11:48:43 2010 +0100 +++ b/src/HOL/Tools/Function/size.ML Thu Jan 28 11:48:49 2010 +0100 @@ -25,7 +25,7 @@ val lookup_size = SizeData.get #> Symtab.lookup; -fun plus (t1, t2) = Const ("HOL.plus_class.plus", +fun plus (t1, t2) = Const (@{const_name Algebras.plus}, HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2; fun size_of_type f g h (T as Type (s, Ts)) =