--- a/src/HOL/Tools/Datatype/datatype_case.ML Mon Nov 30 11:42:49 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Mon Nov 30 12:28:12 2009 +0100
@@ -227,7 +227,6 @@
val nrows = maps (expand constructors used' pty) rows;
val subproblems = partition ty_match ty_inst type_of used'
constructors pty range_ty nrows;
- val new_formals = map #new_formals subproblems
val constructors' = map #constructor subproblems
val news = map (fn {new_formals, group, ...} =>
{path = new_formals @ rstp, rows = group}) subproblems;