1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 22:51:21 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Sun Oct 20 23:29:49 2013 +0200
     1.3 @@ -1068,7 +1068,7 @@
     1.4                    |> K |> Goal.prove lthy [] [] raw_t;
     1.5  val _ = tracing ("raw code theorem: " ^ Syntax.string_of_term lthy (prop_of raw_code_thm));
     1.6                in
     1.7 -                mk_primcorec_code_of_raw_code_tac lthy sel_splits raw_code_thm
     1.8 +                mk_primcorec_code_of_raw_code_tac lthy distincts sel_splits raw_code_thm
     1.9                  |> K |> Goal.prove lthy [] [] t
    1.10  |> tap (tracing o curry (op ^) "code theorem: " o Syntax.string_of_term lthy o prop_of)
    1.11                  |> single