--- 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
--- 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
--- 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
--- 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