src/HOL/Codatatype/Tools/bnf_wrap.ML
changeset 49153 c15a7123605c
parent 49152 feb984727eec
child 49157 6407346b74c7
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 05 11:18:48 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 05 11:37:22 2012 +0200
     1.3 @@ -424,7 +424,7 @@
     1.4              val goal = mk_Trueprop_eq (caseB_fs $ v, mk_rhs discs fs selss);
     1.5            in
     1.6              Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
     1.7 -              mk_case_eq_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss)
     1.8 +              mk_case_eq_tac ctxt n exhaust_thm' case_thms disc_thmss' sel_thmss)
     1.9              |> singleton (Proof_Context.export names_lthy lthy)
    1.10            end;
    1.11