# HG changeset patch
# User wenzelm
# Date 1681997071 -7200
# Node ID dfc1db3f0fcbbd8b21a4d2303f9393ea6ff91f3b
# Parent  44d845b152148df3c3e00bfc40e97d57553f4e45
tuned;

diff -r 44d845b15214 -r dfc1db3f0fcb src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Apr 20 12:50:35 2023 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Apr 20 15:24:31 2023 +0200
@@ -239,7 +239,7 @@
   let val consts = Term.add_const_names (Thm.prop_of th) [] in
     exists (member (op =) (Long_Name.explode s)) forbidden_thms orelse
     exists (member (op =) forbidden_consts) consts orelse
-    length (Long_Name.explode s) <> 2 orelse
+    Long_Name.count s <> 2 orelse
     String.isPrefix "type_definition" (List.last (Long_Name.explode s)) orelse
     String.isSuffix "_def" s orelse
     String.isSuffix "_raw" s orelse
diff -r 44d845b15214 -r dfc1db3f0fcb src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Apr 20 12:50:35 2023 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Apr 20 15:24:31 2023 +0200
@@ -144,7 +144,7 @@
 val mono_timeout = seconds 1.0
 
 fun is_forbidden_theorem name =
-  length (Long_Name.explode name) <> 2 orelse
+  Long_Name.count name <> 2 orelse
   String.isPrefix "type_definition" (List.last (Long_Name.explode name)) orelse
   String.isPrefix "arity_" (List.last (Long_Name.explode name)) orelse
   String.isSuffix "_def" name orelse
diff -r 44d845b15214 -r dfc1db3f0fcb src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Thu Apr 20 12:50:35 2023 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Thu Apr 20 15:24:31 2023 +0200
@@ -71,7 +71,7 @@
     val thy = Proof_Context.theory_of ctxt
     val all_thms =
       thms_of thy thy_name
-      |> filter (fn (name, _) => length (Long_Name.explode name) = 2)  (* FIXME !? *)
+      |> filter (fn (name, _) => Long_Name.count name = 2)  (* FIXME !? *)
       |> sort_by #1
     val check = check_unused_assms ctxt
   in rev (Par_List.map check all_thms) end
diff -r 44d845b15214 -r dfc1db3f0fcb src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Apr 20 12:50:35 2023 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Apr 20 15:24:31 2023 +0200
@@ -484,7 +484,7 @@
           let
             val n = length ths
             val collection = n > 1
-            val dotted_name = length (Long_Name.explode name0) > 2 (* ignore theory name *)
+            val dotted_name = Long_Name.count name0 > 2 (* ignore theory name *)
 
             fun check_thms a =
               (case try (Proof_Context.get_thms ctxt) a of