diff -r 1024dd30da42 -r 7d7d7af647a9 src/HOL/Tools/Function/size.ML
--- 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';