more informative abort

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Oct 21 07:50:32 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Oct 21 08:27:51 2013 +0200
@@ -863,6 +863,7 @@
       corec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy;
     val actual_nn = length bs;
     val corec_specs = take actual_nn corec_specs'; (*###*)
+    val ctr_specss = map #ctr_specs corec_specs;
 
     val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data
       |> partition_eq ((op =) o pairself #fun_name)
@@ -999,7 +1000,7 @@
                 |> single
             end;
 
-        fun prove_code disc_eqns sel_eqns ctr_alist {ctr_specs, ...} =
+        fun prove_code disc_eqns sel_eqns ctr_alist ctr_specs =
           let
             val (fun_name, fun_T, fun_args, maybe_rhs) =
               (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns,
@@ -1044,7 +1045,7 @@
                         maybe_ctr_conds_argss
                         (Const (@{const_name Code.abort}, @{typ String.literal} -->
                             (@{typ unit} --> body_type fun_T) --> body_type fun_T) $
-                          @{term "STR []"} $ (* FIXME *)
+                          HOLogic.mk_literal fun_name $
                           absdummy @{typ unit} (incr_boundvars 1 lhs));
                     in SOME (rhs, rhs, map snd ctr_alist) end
                 end);
@@ -1081,10 +1082,10 @@
         val sel_thmss = map (map snd) sel_alists;
 
         val ctr_alists = map5 (maps oooo prove_ctr) disc_alists sel_alists disc_eqnss sel_eqnss
-          (map #ctr_specs corec_specs);
+          ctr_specss;
         val ctr_thmss = map (map snd) ctr_alists;
 
-        val code_thmss = map4 prove_code disc_eqnss sel_eqnss ctr_alists corec_specs;
+        val code_thmss = map4 prove_code disc_eqnss sel_eqnss ctr_alists ctr_specss;
 
         val simp_thmss = map2 append disc_thmss sel_thmss