diff -r 866cebde3fca -r 9072201cd69d src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Mon Sep 28 09:47:32 2009 +0200
+++ b/src/HOL/Tools/Function/size.ML	Mon Sep 28 10:20:21 2009 +0200
@@ -59,7 +59,7 @@
 
 fun prove_size_thms (info : info) new_type_names thy =
   let
-    val {descr, alt_names, sorts, rec_names, rec_rewrites, inducts = (_, induct), ...} = info;
+    val {descr, alt_names, sorts, rec_names, rec_rewrites, induct, ...} = info;
     val l = length new_type_names;
     val alt_names' = (case alt_names of
       NONE => replicate l NONE | SOME names => map SOME names);