--- a/src/HOL/Tools/Function/size.ML Fri Dec 02 10:31:47 2011 +0100
+++ b/src/HOL/Tools/Function/size.ML Fri Dec 02 13:38:24 2011 +0100
@@ -166,7 +166,7 @@
map (mk_unfolded_size_eq (AList.lookup op =
(new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
(xs ~~ recTs2 ~~ rec_combs2))))
- (fn _ => (indtac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1));
+ (fn _ => (Datatype_Aux.ind_tac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1));
val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs;
val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs';