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/Tools/Mirabelle/mirabelle.ML
changeset 77825 61f652dd955a
parent 77723 b761c91c2447
child 77866 3bd1aa2f3517 
--- 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
isabelle