src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML

   HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
   unfold_thms_tac ctxt (@{thms id_def split comp_def fst_conv snd_conv} @ map_comps @
     map_idents) THEN
   HEADGOAL (rtac refl);
 
-fun prepare_primrec fixes specs lthy =
-  let
-    val thy = Proof_Context.theory_of lthy;
+fun prepare_primrec fixes specs lthy0 =
+  let
+    val thy = Proof_Context.theory_of lthy0;
 
     val (bs, mxs) = map_split (apfst fst) fixes;
     val fun_names = map Binding.name_of bs;
-    val eqns_data = map (dissect_eqn lthy fun_names) specs;
+    val eqns_data = map (dissect_eqn lthy0 fun_names) specs;
     val funs_data = eqns_data
       |> partition_eq ((op =) o pairself #fun_name)
       |> finds (fn (x, y) => x = #fun_name (hd y)) fun_names |> fst
       |> map (fn (x, y) => the_single y
           handle List.Empty =>

     val callssss = funs_data
       |> map (partition_eq ((op =) o pairself #ctr))
       |> map (maps (map_filter (find_rec_calls has_call)));
 
     fun is_only_old_datatype (Type (s, _)) =
-        is_none (fp_sugar_of lthy s) andalso is_some (Datatype_Data.get_info thy s)
+        is_none (fp_sugar_of lthy0 s) andalso is_some (Datatype_Data.get_info thy s)
       | is_only_old_datatype _ = false;
 
     val _ = if exists is_only_old_datatype arg_Ts then raise OLD_PRIMREC () else ();
     val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ res_Ts) of
         [] => ()
       | (b, _) :: _ => primrec_error ("type of " ^ Binding.print b ^ " contains top sort"));
 
-    val ((n2m, rec_specs, _, induct_thm, induct_thms), lthy') =
-      rec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy;
+    val ((n2m, rec_specs, _, induct_thm, induct_thms), lthy) =
+      rec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy0;
 
     val actual_nn = length funs_data;
 
     val _ = let val ctrs = (maps (map #ctr o #ctr_specs) rec_specs) in
       map (fn {ctr, user_eqn, ...} => member (op =) ctrs ctr orelse
-        primrec_error_eqn ("argument " ^ quote (Syntax.string_of_term lthy' ctr) ^
+        primrec_error_eqn ("argument " ^ quote (Syntax.string_of_term lthy ctr) ^
           " is not a constructor in left-hand side") user_eqn) eqns_data end;
 
-    val defs = build_defs lthy' bs mxs funs_data rec_specs has_call;
-
-    fun prove lthy def_thms' ({ctr_specs, nested_map_idents, nested_map_comps, ...} : rec_spec)
+    val defs = build_defs lthy bs mxs funs_data rec_specs has_call;
+
+    fun prove lthy' def_thms' ({ctr_specs, nested_map_idents, nested_map_comps, ...} : rec_spec)
         (fun_data : eqn_data list) =
       let
+        val js =
+          find_indices (op = o pairself (fn {fun_name, ctr, ...} => (fun_name, ctr)))
+            fun_data eqns_data;
+
         val def_thms = map (snd o snd) def_thms';
-        val simp_thmss = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs
+        val simp_thms = finds (fn (x, y) => #ctr x = #ctr y) fun_data ctr_specs
           |> fst
           |> map_filter (try (fn (x, [y]) =>
-            (#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_sorry lthy [] [] user_eqn
-            |> Thm.close_derivation);
-        val poss =
-          find_indices (op = o pairself (fn {fun_name, ctr, ...} => (fun_name, ctr)))
-            fun_data eqns_data;
+            (#fun_name x, #user_eqn x, length (#left_args x) + length (#right_args x), #rec_thm y)))
+          |> map2 (fn j => fn (fun_name, 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_sorry lthy' [] [] user_eqn
+              (* for code extraction from proof terms: *)
+              |> singleton (Proof_Context.export lthy' lthy)
+              |> Thm.name_derivation (Sign.full_name thy (Binding.name fun_name) ^
+                Long_Name.separator ^ simpsN ^
+                (if js = [0] then "" else "_" ^ string_of_int (j + 1))))
+            js;
       in
-        (poss, simp_thmss)
+        (js, simp_thms)
       end;
 
     val notes =
       (if n2m then
          map2 (fn name => fn thm =>

         ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
   in
     (((fun_names, defs),
       fn lthy => fn defs =>
         split_list (map2 (prove lthy defs) (take actual_nn rec_specs) funs_data)),
-      lthy' |> Local_Theory.notes (notes @ common_notes) |> snd)
+      lthy |> Local_Theory.notes (notes @ common_notes) |> snd)
   end;
 
 fun add_primrec_simple fixes ts lthy =
   let
     val (((names, defs), prove), lthy') = prepare_primrec fixes ts lthy

     val _ = null d orelse primrec_error ("duplicate function name(s): " ^ commas d);
 
     val (fixes, specs) = fst (prep_spec raw_fixes raw_spec lthy);
 
     val mk_notes =
-      flat ooo map3 (fn poss => fn prefix => fn thms =>
+      flat ooo map3 (fn js => fn prefix => fn thms =>
         let
-          val (bs, attrss) = map_split (fst o nth specs) poss;
+          val (bs, attrss) = map_split (fst o nth specs) js;
           val notes =
             map3 (fn b => fn attrs => fn thm =>
                 ((Binding.qualify false prefix b, code_nitpicksimp_simp_attrs @ attrs),
                  [([thm], [])]))
               bs attrss thms;

           ((Binding.qualify true prefix (Binding.name simpsN), []), [(thms, [])]) :: notes
         end);
   in
     lthy
     |> add_primrec_simple fixes (map snd specs)
-    |-> (fn (names, (ts, (posss, simpss))) =>
+    |-> (fn (names, (ts, (jss, simpss))) =>
       Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
-      #> Local_Theory.notes (mk_notes posss names simpss)
+      #> Local_Theory.notes (mk_notes jss names simpss)
       #>> pair ts o map snd)
   end
   handle OLD_PRIMREC () => old_primrec raw_fixes raw_spec lthy |>> apsnd single;
 
 val add_primrec = gen_primrec Primrec.add_primrec Specification.check_spec;
 val add_primrec_cmd = gen_primrec Primrec.add_primrec_cmd Specification.read_spec;
 
-fun add_primrec_global fixes specs thy =
-  let
-    val lthy = Named_Target.theory_init thy;
-    val ((ts, simpss), lthy') = add_primrec fixes specs lthy;
-    val simpss' = burrow (Proof_Context.export lthy' lthy) simpss;
-  in ((ts, simpss'), Local_Theory.exit_global lthy') end;
-
-fun add_primrec_overloaded ops fixes specs thy =
-  let
-    val lthy = Overloading.overloading ops thy;
-    val ((ts, simpss), lthy') = add_primrec fixes specs lthy;
-    val simpss' = burrow (Proof_Context.export lthy' lthy) simpss;
-  in ((ts, simpss'), Local_Theory.exit_global lthy') end;
+fun add_primrec_global fixes specs =
+  Named_Target.theory_init
+  #> add_primrec fixes specs
+  ##> Local_Theory.exit_global;
+
+fun add_primrec_overloaded ops fixes specs =
+  Overloading.overloading ops
+  #> add_primrec fixes specs
+  ##> Local_Theory.exit_global;
 
 val _ = Outer_Syntax.local_theory @{command_spec "primrec"}
   "define primitive recursive functions"
   (Parse.fixes -- Parse_Spec.where_alt_specs >> (snd oo uncurry add_primrec_cmd));