diff -r e3fe192fa4a8 -r 61f652dd955a src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Tue Apr 11 15:03:02 2023 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Tue Apr 11 20:32:04 2023 +0200
@@ -302,7 +302,7 @@
 
 fun fold_body_thms f =
   let
-    fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) =>
+    fun app n (PBody {thms, ...}) = thms |> PThms.fold (fn (i, thm_node) =>
       fn (x, seen) =>
         if Inttab.defined seen i then (x, seen)
         else