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/Nitpick_Examples/Mono_Nits.thy
changeset 80306 c2537860ccf8
parent 78709 ebafb2daabb7 
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Sun Jun 09 15:11:07 2024 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Sun Jun 09 15:31:33 2024 +0200
@@ -151,7 +151,7 @@
   String.isSuffix "_raw" name
 
 fun theorems_of thy =
-  filter (fn (name, th) =>
+  filter (fn ((name, _), th) =>
              not (is_forbidden_theorem name) andalso
              Thm.theory_long_name th = Context.theory_long_name thy)
          (Global_Theory.all_thms_of thy true)
@@ -186,7 +186,7 @@
         val (nondef_ts, def_ts, _, _, _, _) =
           Timeout.apply preproc_timeout (preprocess_formulas hol_ctxt [])
                               neg_t
-        val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
+        val res = Thm_Name.print name ^ ": " ^ check_formulas (nondef_ts, def_ts)
       in File.append path (res ^ "\n"); writeln res end
       handle Timeout.TIMEOUT _ => ()
   in thy |> theorems_of |> List.app check_theorem end
isabelle