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 77866 3bd1aa2f3517
parent 77825 61f652dd955a
child 78709 ebafb2daabb7 
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Tue Apr 18 11:45:04 2023 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Tue Apr 18 11:58:12 2023 +0200
@@ -302,7 +302,7 @@
 
 fun fold_body_thms f =
   let
-    fun app n (PBody {thms, ...}) = thms |> PThms.fold (fn (i, thm_node) =>
+    fun app n (PBody {thms, ...}) = thms |> fold (fn (i, thm_node) =>
       fn (x, seen) =>
         if Inttab.defined seen i then (x, seen)
         else
isabelle