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/Predicate_Compile/predicate_compile_data.ML
changeset 82967 73af47bc277c
parent 81510 a14eb229011d 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Aug 07 20:33:28 2025 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Aug 07 21:40:03 2025 +0200
@@ -157,7 +157,9 @@
   let
     val ctxt = Proof_Context.init_global thy
     val inline_defs = Named_Theorems.get ctxt \<^named_theorems>\<open>code_pred_inline\<close>
-    val th' = Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps inline_defs) th
+    val th' =
+      Simplifier.full_simplify
+        (put_simpset HOL_basic_ss ctxt |> Simplifier.add_simps inline_defs) th
     (*val _ = print_step options
       ("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th))
        ^ "with " ^ (commas (map ((Syntax.string_of_term_global thy) o prop_of) inline_defs))
isabelle