diff -r c8c17c2e6ceb -r 3fabf5b5fc83 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Thu Jul 30 13:52:18 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jul 30 15:20:57 2009 +0200
@@ -645,7 +645,7 @@
 
 fun inductive_codegen thy defs dep module brack t gr  = (case strip_comb t of
     (Const ("Collect", _), [u]) =>
-      let val (r, Ts, fs) = HOLogic.strip_splits u
+      let val (r, Ts, fs) = HOLogic.strip_psplits u
       in case strip_comb r of
           (Const (s, T), ts) =>
             (case (get_clauses thy s, get_assoc_code thy (s, T)) of