1.1 --- a/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML	Thu Jan 09 15:07:25 2014 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_rec_sugar.ML	Thu Jan 09 15:08:05 2014 +0100
     1.3 @@ -511,9 +511,9 @@
     1.4              (#user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
     1.5            |> map (fn (user_eqn, num_extra_args, rec_thm) =>
     1.6              mk_primrec_tac lthy num_extra_args nested_map_idents nested_map_comps def_thms rec_thm
     1.7 -            |> K |> Goal.prove lthy [] [] user_eqn
     1.8 +            |> K |> Goal.prove_sorry lthy [] [] user_eqn
     1.9              |> Thm.close_derivation);
    1.10 -        val poss = find_indices (fn (x, y) => #ctr x = #ctr y) fun_data eqns_data;
    1.11 +        val poss = find_indices (op = o pairself #ctr) fun_data eqns_data;
    1.12        in
    1.13          (poss, simp_thmss)
    1.14        end;