src/HOL/Tools/inductive.ML

     val facts =
       map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att lthy) atts), [(thms, [])]))
         args thmss;
     val (res, lthy') = lthy |> Local_Theory.notes facts
     val _ =
-      Proof_Display.print_results
-        {interactive = int, pos = Position.thread_data (), proof_state = false}
+      Proof_Display.print_results {interactive = int, pos = Position.thread_data ()}
         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;

     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));
     val (res, lthy') = lthy |> Local_Theory.notes facts
     val _ =
-      Proof_Display.print_results
-        {interactive = int, pos = Position.thread_data (), proof_state = false}
+      Proof_Display.print_results {interactive = int, pos = Position.thread_data ()}
         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;