Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/simps_case_conv.ML
changeset 82317 231b6d8231c6
parent 80634 a90ab1ea6458 
--- a/src/HOL/Library/simps_case_conv.ML	Fri Mar 21 18:37:05 2025 +0100
+++ b/src/HOL/Library/simps_case_conv.ML	Fri Mar 21 22:26:18 2025 +0100
@@ -117,8 +117,7 @@
     val thm = Attrib.eval_thms lthy thms_ref |> to_case lthy
     val (res, lthy') = Local_Theory.note (bind', [thm]) lthy 
     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 lthy' end
 
@@ -131,8 +130,7 @@
       else gen_to_simps lthy (Attrib.eval_thms lthy splits_ref) thm
     val (res, lthy') = Local_Theory.note (bind', simps) lthy
     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 lthy' end
isabelle