--- a/src/HOL/Real_Asymp/real_asymp.ML Wed Oct 20 16:45:10 2021 +0200
+++ b/src/HOL/Real_Asymp/real_asymp.ML Wed Oct 20 17:11:46 2021 +0200
@@ -72,15 +72,6 @@
val filterlim_substs = map (fn thm => thm RS @{thm filterlim_conv_filtermap}) filter_substs
val eventually_substs = map (fn thm => thm RS @{thm eventually_conv_filtermap}) filter_substs
-fun changed_conv conv ct =
- let
- val thm = conv ct
- in
- if Thm.is_reflexive thm then raise CTERM ("changed_conv", [ct]) else thm
- end
-
-val repeat'_conv = Conv.repeat_conv o changed_conv
-
fun preproc_exp_log_natintfun_conv ctxt =
let
fun reify_power_conv x _ ct =
@@ -100,8 +91,8 @@
Named_Theorems.get ctxt \<^named_theorems>\<open>real_asymp_int_reify\<close>
val ctxt' = put_simpset HOL_basic_ss ctxt addsimps (thms1 @ thms2)
in
- repeat'_conv (
- Simplifier.rewrite ctxt'
+ Conv.repeat_changed_conv
+ (Simplifier.rewrite ctxt'
then_conv Conv.bottom_conv (Conv.try_conv o reify_power_conv (Thm.term_of x)) ctxt)
end
in
--- a/src/Pure/conv.ML Wed Oct 20 16:45:10 2021 +0200
+++ b/src/Pure/conv.ML Wed Oct 20 17:11:46 2021 +0200
@@ -24,6 +24,8 @@
val every_conv: conv list -> conv
val try_conv: conv -> conv
val repeat_conv: conv -> conv
+ val changed_conv: conv -> conv
+ val repeat_changed_conv: conv -> conv
val cache_conv: conv -> conv
val abs_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
val combination_conv: conv -> conv -> conv
@@ -84,6 +86,12 @@
fun try_conv cv = cv else_conv all_conv;
fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct;
+fun changed_conv conv ct =
+ let val th = conv ct
+ in if Thm.is_reflexive th then raise CTERM ("changed_conv", [ct]) else th end;
+
+val repeat_changed_conv = repeat_conv o changed_conv;
+
fun cache_conv (cv: conv) = Ctermtab.cterm_cache cv;