fixed bug in type instantiation of case theorem

--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 05 09:31:31 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 05 09:54:20 2012 +0200
@@ -293,7 +293,7 @@
                   (Drule.instantiate' (map SOME cTs) (map SOME cxs) case_thm)
               end;
             fun mk_thms k xs goal_case case_thm sel_defs =
-              map2 (mk_thm k xs goal_case case_thm) xs sel_defs;
+              map2 (mk_thm k xs (strip_all_body goal_case) case_thm) xs sel_defs;
           in
             map5 mk_thms ks xss goal_cases case_thms sel_defss
           end;