--- a/src/HOL/Tools/function_package/size.ML Wed Jan 21 16:47:03 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML Wed Jan 21 16:47:04 2009 +0100
@@ -144,7 +144,7 @@
(size_names ~~ recTs1))
|> PureThy.add_defs false
(map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
- (def_names ~~ (size_fns ~~ rec_combs1)))
+ (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
||> TheoryTarget.instantiation
(map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
||>> fold_map define_overloaded
@@ -208,7 +208,7 @@
prove_size_eqs is_rec_type overloaded_size_fns (K NONE) simpset3;
val ([size_thms], thy'') = PureThy.add_thmss
- [(("size", size_eqns),
+ [((Binding.name "size", size_eqns),
[Simplifier.simp_add, Thm.declaration_attribute
(fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'