# HG changeset patch
# User blanchet
# Date 1346831660 -7200
# Node ID cb80b6404f8eddb70559c044d8ccc69c982f2009
# Parent  e36ce78add78b8a7bb86902e5679d722d476b752
fixed bug in type instantiation of case theorem

diff -r e36ce78add78 -r cb80b6404f8e src/HOL/Codatatype/Tools/bnf_wrap.ML
--- 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;