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/Nominal/nominal_inductive2.ML
changeset 82643 f1c14af17591
parent 81946 ee680c69de38 
--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed May 21 10:30:33 2025 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed May 21 10:30:34 2025 +0200
@@ -19,10 +19,10 @@
 val inductive_atomize = @{thms induct_atomize};
 val inductive_rulify = @{thms induct_rulify};
 
-fun rulify_term thy = Raw_Simplifier.rewrite_term thy inductive_rulify [];
+fun rulify_term thy = Simplifier.rewrite_term thy inductive_rulify [];
 
 fun atomize_conv ctxt =
-  Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
+  Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
     (put_simpset HOL_basic_ss ctxt addsimps inductive_atomize);
 fun atomize_intr ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (atomize_conv ctxt));
 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
isabelle