# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1709032166 -3600
# Node ID a53287d9add3ab0b0ecfc1230d1f4a12bcabed52
# Parent  6dbe7910dcfc72cd8b63b90b391335f33bd88024
improved output in inductive module;

diff -r 6dbe7910dcfc -r a53287d9add3 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Feb 27 10:49:48 2024 +0100
+++ b/src/HOL/Tools/inductive.ML	Tue Feb 27 12:09:26 2024 +0100
@@ -35,15 +35,15 @@
   val mk_cases: Proof.context -> term -> thm
   val inductive_forall_def: thm
   val rulify: Proof.context -> thm -> thm
-  val inductive_cases: (Attrib.binding * term list) list -> local_theory ->
+  val inductive_cases: (Attrib.binding * term list) list -> bool -> local_theory ->
     (string * thm list) list * local_theory
-  val inductive_cases_cmd: (Attrib.binding * string list) list -> local_theory ->
+  val inductive_cases_cmd: (Attrib.binding * string list) list -> bool -> local_theory ->
     (string * thm list) list * local_theory
   val ind_cases_rules: Proof.context ->
     string list -> (binding * string option * mixfix) list -> thm list
-  val inductive_simps: (Attrib.binding * term list) list -> local_theory ->
+  val inductive_simps: (Attrib.binding * term list) list -> bool -> local_theory ->
     (string * thm list) list * local_theory
-  val inductive_simps_cmd: (Attrib.binding * string list) list -> local_theory ->
+  val inductive_simps_cmd: (Attrib.binding * string list) list -> bool -> local_theory ->
     (string * thm list) list * local_theory
   type flags =
     {quiet_mode: bool, verbose: bool, alt_name: binding, coind: bool,
@@ -606,7 +606,7 @@
 
 (* inductive_cases *)
 
-fun gen_inductive_cases prep_att prep_prop args lthy =
+fun gen_inductive_cases prep_att prep_prop args int lthy =
   let
     val thmss =
       map snd args
@@ -614,7 +614,12 @@
     val facts =
       map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att lthy) atts), [(thms, [])]))
         args thmss;
-  in lthy |> Local_Theory.notes facts end;
+    val (res, lthy') = lthy |> Local_Theory.notes facts
+    val _ =
+      Proof_Display.print_results
+        {interactive = int, pos = Position.thread_data (), proof_state = false}
+        lthy' ((Thm.theoremK, ""), res); 
+  in (res, lthy') end;
 
 val inductive_cases = gen_inductive_cases (K I) Syntax.check_prop;
 val inductive_cases_cmd = gen_inductive_cases Attrib.check_src Syntax.read_prop;
@@ -667,12 +672,17 @@
 
 (* inductive simps *)
 
-fun gen_inductive_simps prep_att prep_prop args lthy =
+fun gen_inductive_simps prep_att prep_prop args int lthy =
   let
     val facts = args |> map (fn ((a, atts), props) =>
       ((a, map (prep_att lthy) atts),
         map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props));
-  in lthy |> Local_Theory.notes facts end;
+    val (res, lthy') = lthy |> Local_Theory.notes facts
+    val _ =
+      Proof_Display.print_results
+        {interactive = int, pos = Position.thread_data (), proof_state = false}
+        lthy' ((Thm.theoremK, ""), res)
+  in (res, lthy') end;
 
 val inductive_simps = gen_inductive_simps (K I) Syntax.check_prop;
 val inductive_simps_cmd = gen_inductive_simps Attrib.check_src Syntax.read_prop;
@@ -1301,14 +1311,14 @@
     (ind_decl true);
 
 val _ =
-  Outer_Syntax.local_theory \<^command_keyword>\<open>inductive_cases\<close>
+  Outer_Syntax.local_theory' \<^command_keyword>\<open>inductive_cases\<close>
     "create simplified instances of elimination rules"
-    (Parse.and_list1 Parse_Spec.simple_specs >> (snd oo inductive_cases_cmd));
+    (Parse.and_list1 Parse_Spec.simple_specs >> (#2 ooo inductive_cases_cmd));
 
 val _ =
-  Outer_Syntax.local_theory \<^command_keyword>\<open>inductive_simps\<close>
+  Outer_Syntax.local_theory' \<^command_keyword>\<open>inductive_simps\<close>
     "create simplification rules for inductive predicates"
-    (Parse.and_list1 Parse_Spec.simple_specs >> (snd oo inductive_simps_cmd));
+    (Parse.and_list1 Parse_Spec.simple_specs >> (#2 ooo inductive_simps_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_inductives\<close>