src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML

     * bool * local_theory
 
   val gfp_rec_sugar_interpretation: string ->
     (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory
 
-  val primcorec_ursive: bool -> corec_option list -> ((binding * typ) * mixfix) list ->
+  val primcorec_ursive: bool -> bool -> corec_option list -> ((binding * typ) * mixfix) list ->
     ((binding * Token.T list list) * term) list -> term option list ->  Proof.context ->
     (term * 'a list) list list * (thm list list -> local_theory -> local_theory) * local_theory
-  val primcorec_ursive_cmd: bool -> corec_option list ->
+  val primcorec_ursive_cmd: bool -> bool -> corec_option list ->
     (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
     Proof.context ->
     (term * 'a list) list list * (thm list list -> local_theory -> local_theory) * local_theory
-  val primcorecursive_cmd: corec_option list ->
+  val primcorecursive_cmd: bool -> corec_option list ->
     (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
     Proof.context -> Proof.state
-  val primcorec_cmd: corec_option list ->
+  val primcorec_cmd: bool -> corec_option list ->
     (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
     local_theory -> local_theory
 end;
 
 structure BNF_GFP_Rec_Sugar : BNF_GFP_REC_SUGAR =

   Term.list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
 
 fun is_trivial_implies thm =
   uncurry (member (op aconv)) (Logic.strip_horn (Thm.prop_of thm));
 
-fun primcorec_ursive auto opts fixes specs of_specs_opt lthy =
+fun primcorec_ursive int auto opts fixes specs of_specs_opt lthy =
   let
     val thy = Proof_Context.theory_of lthy;
 
     val (bs, mxs) = map_split (apfst fst) fixes;
     val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list;

           in
             interpret_gfp_rec_sugar plugins fp_rec_sugar lthy
           end)
       end;
 
-    fun after_qed thmss' = fold_map Local_Theory.define defs #-> prove thmss';
+    fun after_qed thmss' =
+      fold_map Local_Theory.define defs
+      #> tap (uncurry (print_def_consts int))
+      #-> prove thmss';
   in
     (goalss, after_qed, lthy)
   end;
 
-fun primcorec_ursive_cmd auto opts (raw_fixes, raw_specs_of) lthy =
+fun primcorec_ursive_cmd int auto opts (raw_fixes, raw_specs_of) lthy =
   let
     val dups = duplicates (op =) (map (Binding.name_of o #1) raw_fixes);
     val _ = null dups orelse error ("Duplicate function name " ^ quote (hd dups));
 
     val (raw_specs, of_specs_opt) =
       split_list raw_specs_of ||> map (Option.map (Syntax.read_term lthy));
     val (fixes, specs) =
       fst (Specification.read_multi_specs raw_fixes (map (fn spec => (spec, [], [])) raw_specs) lthy);
   in
-    primcorec_ursive auto opts fixes specs of_specs_opt lthy
-  end;
-
-val primcorecursive_cmd = (fn (goalss, after_qed, lthy) =>
-  lthy
-  |> Proof.theorem NONE after_qed goalss
-  |> Proof.refine_singleton (Method.primitive_text (K I))) ooo primcorec_ursive_cmd false;
-
-val primcorec_cmd = (fn (goalss, after_qed, lthy) =>
+    primcorec_ursive int auto opts fixes specs of_specs_opt lthy
+  end;
+
+fun primcorecursive_cmd int = (fn (goalss, after_qed, lthy) =>
+    lthy
+    |> Proof.theorem NONE after_qed goalss
+    |> Proof.refine_singleton (Method.primitive_text (K I))) ooo
+  primcorec_ursive_cmd int false;
+
+fun primcorec_cmd int = (fn (goalss, after_qed, lthy) =>
     lthy |> after_qed (map (fn [] => [] | _ => use_primcorecursive ()) goalss)) ooo
-  primcorec_ursive_cmd true;
+  primcorec_ursive_cmd int true;
 
 val corec_option_parser = Parse.group (K "option")
   (Plugin_Name.parse_filter >> Plugins_Option
    || Parse.reserved "sequential" >> K Sequential_Option
    || Parse.reserved "exhaustive" >> K Exhaustive_Option

 
 val _ = Outer_Syntax.local_theory_to_proof @{command_keyword primcorecursive}
   "define primitive corecursive functions"
   ((Scan.optional (@{keyword "("} |--
       Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) --
-    (Parse.vars -- where_alt_props_of_parser) >> uncurry primcorecursive_cmd);
+    (Parse.vars -- where_alt_props_of_parser) >> uncurry (primcorecursive_cmd true));
 
 val _ = Outer_Syntax.local_theory @{command_keyword primcorec}
   "define primitive corecursive functions"
   ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
       --| @{keyword ")"}) []) --
-    (Parse.vars -- where_alt_props_of_parser) >> uncurry primcorec_cmd);
+    (Parse.vars -- where_alt_props_of_parser) >> uncurry (primcorec_cmd true));
 
 val _ = Theory.setup (gfp_rec_sugar_interpretation transfer_plugin
   gfp_rec_sugar_transfer_interpretation);
 
 end;