print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'

--- a/src/HOL/Inductive.thy	Mon Dec 26 15:31:13 2016 +0100
+++ b/src/HOL/Inductive.thy	Wed Dec 28 17:22:16 2016 +0100
@@ -519,9 +519,8 @@
 ML_file "Tools/Old_Datatype/old_datatype_data.ML"
 ML_file "Tools/Old_Datatype/old_rep_datatype.ML"
 ML_file "Tools/Old_Datatype/old_datatype_codegen.ML"
+ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
 ML_file "Tools/Old_Datatype/old_primrec.ML"
-
-ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
 ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
 
 text \<open>Lambda-abstractions with pattern matching:\<close>

--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Mon Dec 26 15:31:13 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML	Wed Dec 28 17:22:16 2016 +0100
@@ -56,6 +56,8 @@
 
   val mk_conjunctN: int -> int -> thm
   val conj_dests: int -> thm -> thm list
+
+  val print_def_consts: bool -> (term * (string * thm)) list -> Proof.context -> unit
 end;
 
 structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL =
@@ -174,4 +176,8 @@
 
 fun conj_dests n thm = map (fn k => thm RS mk_conjunctN n k) (1 upto n);
 
+fun print_def_consts int defs ctxt =
+  Proof_Display.print_consts int (Position.thread_data ()) ctxt (K false)
+    (map_filter (try (dest_Free o fst)) defs);
+
 end;

--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Mon Dec 26 15:31:13 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Wed Dec 28 17:22:16 2016 +0100
@@ -261,7 +261,7 @@
     val (([free], [def_free], [simps_free]), (lthy, lthy_old)) = lthy
       |> Local_Theory.open_target |> snd
       |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed) (*TODO check*)
-      |> primrec [] [(b, NONE, NoSyn)] (map (fn eq => ((Binding.empty_atts, eq), [], [])) eqs)
+      |> primrec false [] [(b, NONE, NoSyn)] (map (fn eq => ((Binding.empty_atts, eq), [], [])) eqs)
       ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;

--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Mon Dec 26 15:31:13 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Wed Dec 28 17:22:16 2016 +0100
@@ -23,10 +23,10 @@
   val derive_unique: Proof.context -> morphism -> term -> BNF_GFP_Grec.corec_info -> string ->
     thm -> thm
 
-  val corec_cmd: corec_option list -> (binding * string option * mixfix) list * string ->
+  val corec_cmd: bool -> corec_option list -> (binding * string option * mixfix) list * string ->
     local_theory -> local_theory
-  val corecursive_cmd: corec_option list -> (binding * string option * mixfix) list * string ->
-    local_theory -> Proof.state
+  val corecursive_cmd: bool -> corec_option list ->
+    (binding * string option * mixfix) list * string -> local_theory -> Proof.state
   val friend_of_corec_cmd: (string * string option) * string -> local_theory -> Proof.state
   val coinduction_upto_cmd: string * string -> local_theory -> local_theory
 end;
@@ -1995,7 +1995,7 @@
       else
         ((false, extras), lthy));
 
-fun prepare_corec_ursive_cmd long_cmd opts (raw_fixes, raw_eq) lthy =
+fun prepare_corec_ursive_cmd int long_cmd opts (raw_fixes, raw_eq) lthy =
   let
     val _ = can the_single raw_fixes orelse
       error "Mutually corecursive functions not supported";
@@ -2090,6 +2090,7 @@
         val ((fun_t0, (_, fun_def0)), (lthy, lthy_old)) = lthy
           |> Local_Theory.open_target |> snd
           |> Local_Theory.define def
+          |> tap (fn (def, lthy) => print_def_consts int [def] lthy)
           ||> `Local_Theory.close_target;
 
         val parsed_eq = parse_corec_equation lthy [fun_free] eq;
@@ -2217,11 +2218,11 @@
         (inner_fp_triple, termin_goals), (const_transfers, const_transfer_goals'))), lthy)
   end;
 
-fun corec_cmd opts (raw_fixes, raw_eq) lthy =
+fun corec_cmd int opts (raw_fixes, raw_eq) lthy =
   let
     val ((def_fun, (_, (inner_fp_triple, termin_goals), (const_transfers, const_transfer_goals))),
          lthy) =
-      prepare_corec_ursive_cmd false opts (raw_fixes, raw_eq) lthy;
+      prepare_corec_ursive_cmd int false opts (raw_fixes, raw_eq) lthy;
   in
     if not (null termin_goals) then
       error ("Termination prover failed (try " ^ quote (#1 @{command_keyword corecursive}) ^
@@ -2233,11 +2234,11 @@
       def_fun inner_fp_triple const_transfers [] lthy
   end;
 
-fun corecursive_cmd opts (raw_fixes, raw_eq) lthy =
+fun corecursive_cmd int opts (raw_fixes, raw_eq) lthy =
   let
     val ((def_fun, (([Type (fpT_name, _)], prepareds, rho_datas, rho_transfer_goals),
             (inner_fp_triple, termin_goals), (const_transfers, const_transfer_goals))), lthy) =
-      prepare_corec_ursive_cmd true opts (raw_fixes, raw_eq) lthy;
+      prepare_corec_ursive_cmd int true opts (raw_fixes, raw_eq) lthy;
 
     val (rho_transfer_goals', unprime_rho_transfer_and_folds) =
       @{map 3} (fn (_, _, _, _, _, _, _, _, _, _, _, _, _) => fn (_, rho_def) =>
@@ -2403,13 +2404,13 @@
   "define nonprimitive corecursive functions"
   ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
       --| @{keyword ")"}) []) -- (Parse.vars --| Parse.where_ -- Parse.prop)
-   >> uncurry corec_cmd);
+   >> uncurry (corec_cmd true));
 
 val _ = Outer_Syntax.local_theory_to_proof @{command_keyword corecursive}
   "define nonprimitive corecursive functions"
   ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
       --| @{keyword ")"}) []) -- (Parse.vars --| Parse.where_ -- Parse.prop)
-   >> uncurry corecursive_cmd);
+   >> uncurry (corecursive_cmd true));
 
 val _ = Outer_Syntax.local_theory_to_proof @{command_keyword friend_of_corec}
   "register a function as a legal context for nonprimitive corecursion"

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Dec 26 15:31:13 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Dec 28 17:22:16 2016 +0100
@@ -82,17 +82,17 @@
   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;
@@ -1082,7 +1082,7 @@
 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;
 
@@ -1581,12 +1581,15 @@
           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));
@@ -1596,17 +1599,18 @@
     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
+    primcorec_ursive int 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;
+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;
 
-val primcorec_cmd = (fn (goalss, after_qed, lthy) =>
+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
@@ -1621,13 +1625,13 @@
   "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);

--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Dec 26 15:31:13 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Dec 28 17:22:16 2016 +0100
@@ -538,11 +538,11 @@
 
 fun old_of_new f (ts, _, simpss) = (ts, f simpss);
 
-val primrec = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec [];
-val primrec_global = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec_global [];
-val primrec_overloaded = apfst (old_of_new flat) oooo BNF_LFP_Rec_Sugar.primrec_overloaded [];
+val primrec = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec false [];
+val primrec_global = apfst (old_of_new flat) ooo BNF_LFP_Rec_Sugar.primrec_global false [];
+val primrec_overloaded = apfst (old_of_new flat) oooo BNF_LFP_Rec_Sugar.primrec_overloaded false [];
 val primrec_simple = apfst (apfst fst o apsnd (old_of_new (flat o snd))) ooo
-  BNF_LFP_Rec_Sugar.primrec_simple;
+  BNF_LFP_Rec_Sugar.primrec_simple false;
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword datatype_compat}

--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Dec 26 15:31:13 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Dec 28 17:22:16 2016 +0100
@@ -62,21 +62,20 @@
   val lfp_rec_sugar_interpretation: string ->
     (BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> local_theory -> local_theory) -> theory -> theory
 
-  val primrec: rec_option list -> (binding * typ option * mixfix) list ->
+  val primrec: bool -> rec_option list -> (binding * typ option * mixfix) list ->
     Specification.multi_specs -> local_theory ->
     (term list * thm list * thm list list) * local_theory
-  val primrec_cmd: rec_option list -> (binding * string option * mixfix) list ->
+  val primrec_cmd: bool -> rec_option list -> (binding * string option * mixfix) list ->
     Specification.multi_specs_cmd -> local_theory ->
     (term list * thm list * thm list list) * local_theory
-  val primrec_global: rec_option list -> (binding * typ option * mixfix) list ->
+  val primrec_global: bool -> rec_option list -> (binding * typ option * mixfix) list ->
     Specification.multi_specs -> theory -> (term list * thm list * thm list list) * theory
-  val primrec_overloaded: rec_option list -> (string * (string * typ) * bool) list ->
+  val primrec_overloaded: bool -> rec_option list -> (string * (string * typ) * bool) list ->
     (binding * typ option * mixfix) list ->
     Specification.multi_specs -> theory -> (term list * thm list * thm list list) * theory
-  val primrec_simple: ((binding * typ) * mixfix) list -> term list ->
-    local_theory ->
-    ((string list * (binding -> binding) list) *
-    (term list * thm list * (int list list * thm list list))) * local_theory
+  val primrec_simple: bool -> ((binding * typ) * mixfix) list -> term list -> local_theory ->
+    ((string list * (binding -> binding) list)
+     * (term list * thm list * (int list list * thm list list))) * local_theory
 end;
 
 structure BNF_LFP_Rec_Sugar : BNF_LFP_REC_SUGAR =
@@ -179,6 +178,8 @@
     in
       ([], [0], [basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, ctxt)
     end
+  | default_basic_lfp_sugars_of _ [T] _ _ ctxt =
+    error ("Cannot recurse through type " ^ quote (Syntax.string_of_typ ctxt T))
   | default_basic_lfp_sugars_of _ _ _ _ _ = error "Unsupported mutual recursion at this stage";
 
 fun basic_lfp_sugars_of bs arg_Ts callers callssss lthy =
@@ -605,7 +606,7 @@
       lthy |> Local_Theory.notes (notes @ common_notes) |> snd)
   end;
 
-fun primrec_simple0 plugins nonexhaustive transfer fixes ts lthy =
+fun primrec_simple0 int plugins nonexhaustive transfer fixes ts lthy =
   let
     val actual_nn = length fixes;
 
@@ -617,20 +618,21 @@
   in
     lthy'
     |> fold_map Local_Theory.define defs
+    |> tap (uncurry (print_def_consts int))
     |-> (fn defs => fn lthy =>
       let val ((jss, simpss), lthy) = prove lthy defs in
         (((names, qualifys), (map fst defs, map (snd o snd) defs, (jss, simpss))), lthy)
       end)
   end;
 
-fun primrec_simple fixes ts lthy =
-  primrec_simple0 Plugin_Name.default_filter false false fixes ts lthy
+fun primrec_simple int fixes ts lthy =
+  primrec_simple0 int Plugin_Name.default_filter false false fixes ts lthy
   handle OLD_PRIMREC () =>
-    Old_Primrec.primrec_simple fixes ts lthy
+    Old_Primrec.primrec_simple int fixes ts lthy
     |>> apsnd (fn (ts, thms) => (ts, [], ([], [thms]))) o apfst single
     |>> apfst (map_split (rpair I));
 
-fun gen_primrec old_primrec prep_spec opts raw_fixes raw_specs lthy =
+fun gen_primrec old_primrec prep_spec int opts raw_fixes raw_specs lthy =
   let
     val dups = duplicates (op =) (map (fn (x, _, _) => Binding.name_of x) raw_fixes);
     val _ = null dups orelse error ("Duplicate function name " ^ quote (hd dups));
@@ -658,27 +660,27 @@
         end);
   in
     lthy
-    |> primrec_simple0 plugins nonexhaustive transfer fixes (map snd specs)
+    |> primrec_simple0 int plugins nonexhaustive transfer fixes (map snd specs)
     |-> (fn ((names, qualifys), (ts, defs, (jss, simpss))) =>
       Spec_Rules.add Spec_Rules.Equational (ts, flat simpss)
       #> Local_Theory.notes (mk_notes jss names qualifys simpss)
       #>> (fn notes => (ts, defs, map_filter (fn ("", _) => NONE | (_, thms) => SOME thms) notes)))
   end
   handle OLD_PRIMREC () =>
-    old_primrec raw_fixes raw_specs lthy
+    old_primrec int raw_fixes raw_specs lthy
     |>> (fn (ts, thms) => (ts, [], [thms]));
 
 val primrec = gen_primrec Old_Primrec.primrec Specification.check_multi_specs;
 val primrec_cmd = gen_primrec Old_Primrec.primrec_cmd Specification.read_multi_specs;
 
-fun primrec_global opts fixes specs =
+fun primrec_global int opts fixes specs =
   Named_Target.theory_init
-  #> primrec opts fixes specs
+  #> primrec int opts fixes specs
   ##> Local_Theory.exit_global;
 
-fun primrec_overloaded opts ops fixes specs =
+fun primrec_overloaded int opts ops fixes specs =
   Overloading.overloading ops
-  #> primrec opts fixes specs
+  #> primrec int opts fixes specs
   ##> Local_Theory.exit_global;
 
 val rec_option_parser = Parse.group (K "option")
@@ -690,6 +692,6 @@
   "define primitive recursive functions"
   ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 rec_option_parser)
       --| @{keyword ")"}) []) -- Parse_Spec.specification
-    >> (fn (opts, (fixes, specs)) => snd o primrec_cmd opts fixes specs));
+    >> (fn (opts, (fixes, specs)) => snd o primrec_cmd true opts fixes specs));
 
 end;

--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Mon Dec 26 15:31:13 2016 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Wed Dec 28 17:22:16 2016 +0100
@@ -8,16 +8,16 @@
 
 signature OLD_PRIMREC =
 sig
-  val primrec: (binding * typ option * mixfix) list ->
+  val primrec: bool -> (binding * typ option * mixfix) list ->
     Specification.multi_specs -> local_theory -> (term list * thm list) * local_theory
-  val primrec_cmd: (binding * string option * mixfix) list ->
+  val primrec_cmd: bool -> (binding * string option * mixfix) list ->
     Specification.multi_specs_cmd -> local_theory -> (term list * thm list) * local_theory
-  val primrec_global: (binding * typ option * mixfix) list ->
+  val primrec_global: bool -> (binding * typ option * mixfix) list ->
     Specification.multi_specs -> theory -> (term list * thm list) * theory
-  val primrec_overloaded: (string * (string * typ) * bool) list ->
+  val primrec_overloaded: bool -> (string * (string * typ) * bool) list ->
     (binding * typ option * mixfix) list ->
     Specification.multi_specs -> theory -> (term list * thm list) * theory
-  val primrec_simple: ((binding * typ) * mixfix) list -> term list ->
+  val primrec_simple: bool -> ((binding * typ) * mixfix) list -> term list ->
     local_theory -> (string * (term list * thm list)) * local_theory
 end;
 
@@ -188,12 +188,12 @@
       in
         (dummy_fns @ fs, defs)
       end
-  | SOME (fname, ls, fs') => (fs' @ fs, (fname, ls, rec_name, tname) :: defs));
+  | SOME (fname, ls, fs') => (fs' @ fs, (fname, ls, rec_name) :: defs));
 
 
 (* make definition *)
 
-fun make_def ctxt fixes fs (fname, ls, rec_name, tname) =
+fun make_def ctxt fixes fs (fname, ls, rec_name) =
   let
     val SOME (var, varT) = get_first (fn ((b, T), mx) =>
       if Binding.name_of b = fname then SOME ((b, mx), T) else NONE) fixes;
@@ -260,18 +260,19 @@
 
 (* primrec definition *)
 
-fun primrec_simple fixes ts lthy =
+fun primrec_simple int fixes ts lthy =
   let
     val ((prefix, (_, defs)), prove) = distill lthy fixes ts;
   in
     lthy
     |> fold_map Local_Theory.define defs
+    |> tap (uncurry (BNF_FP_Rec_Sugar_Util.print_def_consts int))
     |-> (fn defs => `(fn lthy => (prefix, (map fst defs, prove lthy defs))))
   end;
 
 local
 
-fun gen_primrec prep_spec raw_fixes raw_spec lthy =
+fun gen_primrec prep_spec int raw_fixes raw_spec lthy =
   let
     val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
     fun attr_bindings prefix = map (fn ((b, attrs), _) =>
@@ -280,7 +281,7 @@
       (Binding.qualify true prefix (Binding.name "simps"), @{attributes [simp, nitpick_simp]});
   in
     lthy
-    |> primrec_simple fixes (map snd spec)
+    |> primrec_simple int fixes (map snd spec)
     |-> (fn (prefix, (ts, simps)) =>
       Spec_Rules.add Spec_Rules.Equational (ts, simps)
       #> fold_map Local_Theory.note (attr_bindings prefix ~~ map single simps)
@@ -295,17 +296,17 @@
 
 end;
 
-fun primrec_global fixes specs thy =
+fun primrec_global int fixes specs thy =
   let
     val lthy = Named_Target.theory_init thy;
-    val ((ts, simps), lthy') = primrec fixes specs lthy;
+    val ((ts, simps), lthy') = primrec int fixes specs lthy;
     val simps' = Proof_Context.export lthy' lthy simps;
   in ((ts, simps'), Local_Theory.exit_global lthy') end;
 
-fun primrec_overloaded ops fixes specs thy =
+fun primrec_overloaded int ops fixes specs thy =
   let
     val lthy = Overloading.overloading ops thy;
-    val ((ts, simps), lthy') = primrec fixes specs lthy;
+    val ((ts, simps), lthy') = primrec int fixes specs lthy;
     val simps' = Proof_Context.export lthy' lthy simps;
   in ((ts, simps'), Local_Theory.exit_global lthy') end;