--- 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);