src/HOL/Codatatype/Tools/bnf_wrap.ML

--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 05 11:18:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 05 11:37:22 2012 +0200
@@ -424,7 +424,7 @@
             val goal = mk_Trueprop_eq (caseB_fs $ v, mk_rhs discs fs selss);
           in
             Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
-              mk_case_eq_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss)
+              mk_case_eq_tac ctxt n exhaust_thm' case_thms disc_thmss' sel_thmss)
             |> singleton (Proof_Context.export names_lthy lthy)
           end;