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/Pure/Isar/object_logic.ML
changeset 82641 d22294b20573
parent 81519 cdc43c0fdbfc 
--- a/src/Pure/Isar/object_logic.ML	Wed May 21 10:30:06 2025 +0200
+++ b/src/Pure/Isar/object_logic.ML	Wed May 21 10:30:07 2025 +0200
@@ -203,7 +203,7 @@
   drop_judgment ctxt o
     Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) (get_atomize ctxt) [];
 
-fun atomize ctxt = Raw_Simplifier.rewrite ctxt true (get_atomize ctxt);
+fun atomize ctxt = Raw_Simplifier.rewrite_wrt ctxt true (get_atomize ctxt);
 
 fun atomize_prems ctxt ct =
   if Logic.has_meta_prems (Thm.term_of ct) then
@@ -222,7 +222,7 @@
 fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify ctxt);
 
 fun gen_rulify full ctxt =
-  Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify ctxt))
+  Conv.fconv_rule (Raw_Simplifier.rewrite_wrt ctxt full (get_rulify ctxt))
   #> Variable.gen_all ctxt
   #> Thm.strip_shyps
   #> Drule.zero_var_indexes;
isabelle