tuned: more standard Isabelle/ML;
authorwenzelm
Sun, 04 Aug 2024 23:17:35 +0200 (5 months ago)
changeset 80639 3322b6ae6b19
parent 80638 21637b691fab
child 80640 3cde955e4e47
tuned: more standard Isabelle/ML;
src/HOL/Tools/cnf.ML
--- a/src/HOL/Tools/cnf.ML	Sun Aug 04 22:59:51 2024 +0200
+++ b/src/HOL/Tools/cnf.ML	Sun Aug 04 23:17:35 2024 +0200
@@ -447,17 +447,15 @@
     val simp_thm = simp_True_False_thm ctxt nnf
     val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) simp_thm
     (* initialize var_id, in case the term already contains variables of the form "cnfx_<int>" *)
-    val _ = (var_id := fold (fn free => fn max =>
+    val _ = (var_id := Frees.fold (fn ((name, _), _) => fn max =>
       let
-        val (name, _) = dest_Free free
         val idx =
-          if String.isPrefix "cnfx_" name then
-            (Int.fromString o String.extract) (name, String.size "cnfx_", NONE)
-          else
-            NONE
+          (case try (unprefix "cnfx_") name of
+            SOME s => Int.fromString s
+          | NONE => NONE)
       in
         Int.max (max, the_default 0 idx)
-      end) (Misc_Legacy.term_frees simp) 0)
+      end) (Frees.build (Frees.add_frees simp)) 0)
     (* finally, convert to definitional CNF (this should preserve the simplification) *)
     val cnfx_thm = make_under_quantifiers ctxt make_cnfx_thm_from_nnf simp
 (*###