# HG changeset patch
# User blanchet
# Date 1392388783 -3600
# Node ID 61ffc2339a8cc7e92c295a8b3b3079d01bd3bca2
# Parent  a8b83356e869fc1b2ae852279eeb98433f325192
removed assumption in 'primrec_new' that a given constructor can only occur once

diff -r a8b83356e869 -r 61ffc2339a8c src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Feb 14 15:14:35 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Feb 14 15:39:43 2014 +0100
@@ -513,14 +513,19 @@
             mk_primrec_tac lthy num_extra_args nested_map_idents nested_map_comps def_thms rec_thm
             |> K |> Goal.prove_sorry lthy [] [] user_eqn
             |> Thm.close_derivation);
-        val poss = find_indices (op = o pairself #ctr) fun_data eqns_data;
+        val poss =
+          find_indices (op = o pairself (fn {fun_name, ctr, ...} => (fun_name, ctr)))
+            fun_data eqns_data;
       in
         (poss, simp_thmss)
       end;
 
     val notes =
-      (if n2m then map2 (fn name => fn thm =>
-        (name, inductN, [thm], [])) fun_names (take actual_nn induct_thms) else [])
+      (if n2m then
+         map2 (fn name => fn thm =>
+           (name, inductN, [thm], [])) fun_names (take actual_nn induct_thms)
+       else
+         [])
       |> map (fn (prefix, thmN, thms, attrs) =>
         ((Binding.qualify true prefix (Binding.name thmN), attrs), [(thms, [])]));