# HG changeset patch
# User wenzelm
# Date 1634742706 -7200
# Node ID 5c8177fd1295757556a29f00902912ec7009b8c3
# Parent  9189d949abb90bf64cf54e1f21404db201142ac4
clarified modules;

diff -r 9189d949abb9 -r 5c8177fd1295 src/HOL/Real_Asymp/real_asymp.ML
--- 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
diff -r 9189d949abb9 -r 5c8177fd1295 src/Pure/conv.ML
--- 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;