use 'prove_sorry'

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