diff --git a/src/HOL/Real_Asymp/real_asymp.ML b/src/HOL/Real_Asymp/real_asymp.ML
--- a/src/HOL/Real_Asymp/real_asymp.ML
+++ b/src/HOL/Real_Asymp/real_asymp.ML
@@ -1,200 +1,191 @@
 signature REAL_ASYMP = sig
 val tac : bool -> Proof.context -> int -> tactic
 end
 
 functor Real_Asymp (Exp : EXPANSION_INTERFACE) : REAL_ASYMP = struct
 
 open Lazy_Eval
 
 val dest_arg = dest_comb #> snd
 
 fun prove_limit_at_top ectxt f filter =
   let
     val ctxt = get_ctxt ectxt
     val basis = Asymptotic_Basis.default_basis
     val prover =
       case filter of
         Const (\<^const_name>\<open>Topological_Spaces.nhds\<close>, _) $ _ => SOME Exp.prove_nhds
       | \<^term>\<open>at (0 :: real)\<close> => SOME Exp.prove_at_0
       | \<^term>\<open>at_left (0 :: real)\<close> => SOME Exp.prove_at_left_0
       | \<^term>\<open>at_right (0 :: real)\<close> => SOME Exp.prove_at_right_0
       | \<^term>\<open>at_infinity :: real filter\<close> => SOME Exp.prove_at_infinity
       | \<^term>\<open>at_top :: real filter\<close> => SOME Exp.prove_at_top
       | \<^term>\<open>at_bot :: real filter\<close> => SOME Exp.prove_at_bot
       | _ => NONE
     val lim_thm = Option.map (fn prover => prover ectxt (Exp.expand_term ectxt f basis)) prover
   in
     case lim_thm of
       NONE => no_tac
     | SOME lim_thm =>
         HEADGOAL (
           resolve_tac ctxt [lim_thm, lim_thm RS @{thm filterlim_mono'}]
           THEN_ALL_NEW (TRY o resolve_tac ctxt @{thms at_within_le_nhds at_within_le_at nhds_leI}))
   end
 
 fun prove_eventually_at_top ectxt p =
   case Envir.eta_long [] p of
     Abs (x, \<^typ>\<open>Real.real\<close>, Const (rel, _) $ f $ g) => ((
       let
         val (f, g) = apply2 (fn t => Abs (x, \<^typ>\<open>Real.real\<close>, t)) (f, g)
         val _ = if rel = \<^const_name>\<open>Orderings.less\<close> 
                     orelse rel = \<^const_name>\<open>Orderings.less_eq\<close> then ()
                   else raise TERM ("prove_eventually_at_top", [p])
         val ctxt = get_ctxt ectxt
         val basis = Asymptotic_Basis.default_basis
         val ([thm1, thm2], basis) = Exp.expand_terms ectxt [f, g] basis
         val thm = Exp.prove_eventually_less ectxt (thm1, thm2, basis)
       in
         HEADGOAL (resolve_tac ctxt [thm, thm RS @{thm eventually_lt_imp_eventually_le}])
       end)
     handle TERM _ => no_tac | THM _ => no_tac)
   | _ => raise TERM ("prove_eventually_at_top", [p])
 
 fun prove_landau ectxt l f g =
   let
     val ctxt = get_ctxt ectxt
     val l' = l |> dest_Const |> fst
     val basis = Asymptotic_Basis.default_basis
     val ([thm1, thm2], basis) = Exp.expand_terms ectxt [f, g] basis
     val prover =
       case l' of
         \<^const_name>\<open>smallo\<close> => Exp.prove_smallo
       | \<^const_name>\<open>bigo\<close> => Exp.prove_bigo
       | \<^const_name>\<open>bigtheta\<close> => Exp.prove_bigtheta
       | \<^const_name>\<open>asymp_equiv\<close> => Exp.prove_asymp_equiv
       | _ => raise TERM ("prove_landau", [f, g])
   in
     HEADGOAL (resolve_tac ctxt [prover ectxt (thm1, thm2, basis)])
   end
 
 val filter_substs = 
   @{thms at_left_to_top at_right_to_top at_left_to_top' at_right_to_top' at_bot_mirror}
 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 =
       let
         val thm = Conv.rewr_conv @{thm reify_power} ct
       in
         if exists_subterm (fn t => t aconv x) (Thm.term_of ct |> dest_arg) then
           thm
         else
           raise CTERM ("reify_power_conv", [ct])
       end
     fun conv (x, ctxt) =
       let
         val thms1 =
            Named_Theorems.get ctxt \<^named_theorems>\<open>real_asymp_nat_reify\<close>
         val thms2 =
            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
     Thm.eta_long_conversion
     then_conv Conv.abs_conv conv ctxt 
     then_conv Thm.eta_conversion
   end
 
 fun preproc_tac ctxt =
   let
     fun natint_tac {context = ctxt, concl = goal, ...} =
       let
         val conv = preproc_exp_log_natintfun_conv ctxt
         val conv =
           case Thm.term_of goal of
             \<^term>\<open>HOL.Trueprop\<close> $ t => (case t of
               Const (\<^const_name>\<open>Filter.filterlim\<close>, _) $ _ $ _ $ _ =>
                 Conv.fun_conv (Conv.fun_conv (Conv.arg_conv conv))
             | Const (\<^const_name>\<open>Filter.eventually\<close>, _) $ _ $ _ =>
                 Conv.fun_conv (Conv.arg_conv conv)
             | Const (\<^const_name>\<open>Set.member\<close>, _) $ _ $ (_ $ _ $ _) =>
                 Conv.combination_conv (Conv.arg_conv conv) (Conv.arg_conv conv)
             | Const (\<^const_name>\<open>Landau_Symbols.asymp_equiv\<close>, _) $ _ $ _ $ _ =>
                 Conv.combination_conv (Conv.fun_conv (Conv.arg_conv conv)) conv
             | _ => Conv.all_conv)
           | _ => Conv.all_conv
       in
         HEADGOAL (CONVERSION (Conv.try_conv (Conv.arg_conv conv)))
       end
   in
     SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms real_asymp_preproc})
     THEN' TRY o resolve_tac ctxt @{thms real_asymp_real_nat_transfer real_asymp_real_int_transfer}
     THEN' TRY o resolve_tac ctxt 
       @{thms filterlim_at_leftI filterlim_at_rightI filterlim_atI' landau_reduce_to_top}
     THEN' TRY o resolve_tac ctxt @{thms smallo_imp_smallomega bigo_imp_bigomega}
     THEN' TRY o Subgoal.FOCUS_PREMS natint_tac ctxt
     THEN' TRY o resolve_tac ctxt @{thms real_asymp_nat_intros real_asymp_int_intros}
   end
 
 datatype ('a, 'b) sum = Inl of 'a | Inr of 'b
 
 fun prove_eventually ectxt p filter =
   case filter of
     \<^term>\<open>Filter.at_top :: real filter\<close> => (prove_eventually_at_top ectxt p
       handle TERM _ => no_tac | THM _ => no_tac)
   | _ => HEADGOAL (CONVERSION (Conv.rewrs_conv eventually_substs) 
          THEN' tac' (#verbose (#ctxt ectxt)) (Inr ectxt))
 and prove_limit ectxt f filter filter' =
   case filter' of
     \<^term>\<open>Filter.at_top :: real filter\<close> => (prove_limit_at_top ectxt f filter 
       handle TERM _ => no_tac | THM _ => no_tac)
   | _ => HEADGOAL (CONVERSION (Conv.rewrs_conv filterlim_substs) 
          THEN' tac' (#verbose (#ctxt ectxt)) (Inr ectxt))
 and tac' verbose ctxt_or_ectxt =
   let
     val ctxt = case ctxt_or_ectxt of Inl ctxt => ctxt | Inr ectxt => get_ctxt ectxt
     fun tac {context = ctxt, prems, concl = goal, ...} =
       (if verbose then print_tac ctxt "real_asymp: Goal after preprocessing" else all_tac) THEN
       let
         val ectxt = 
           case ctxt_or_ectxt of 
             Inl _ => 
               Multiseries_Expansion.mk_eval_ctxt ctxt |> add_facts prems |> set_verbose verbose
           | Inr ectxt => ectxt
       in
         case Thm.term_of goal of
           \<^term>\<open>HOL.Trueprop\<close> $ t => ((case t of
             \<^term>\<open>Filter.filterlim :: (real \<Rightarrow> real) \<Rightarrow> _\<close> $ f $ filter $ filter' =>
               (prove_limit ectxt f filter filter' handle TERM _ => no_tac | THM _ => no_tac)
           | \<^term>\<open>Filter.eventually :: (real \<Rightarrow> bool) \<Rightarrow> _\<close> $ p $ filter =>
               (prove_eventually ectxt p filter handle TERM _ => no_tac | THM _ => no_tac)
           | \<^term>\<open>Set.member :: (real => real) => _\<close> $ f $ 
               (l $ \<^term>\<open>at_top :: real filter\<close> $ g) =>
                 (prove_landau ectxt l f g handle TERM _ => no_tac | THM _ => no_tac)
           | (l as \<^term>\<open>Landau_Symbols.asymp_equiv :: (real\<Rightarrow>real)\<Rightarrow>_\<close>) $ f $ _ $ g =>
               (prove_landau ectxt l f g handle TERM _ => no_tac | THM _ => no_tac)
           | _ => no_tac) THEN distinct_subgoals_tac)
         | _ => no_tac
       end
     fun tac' i = Subgoal.FOCUS_PREMS tac ctxt i handle TERM _ => no_tac | THM _ => no_tac
     val at_tac =
       HEADGOAL (resolve_tac ctxt 
         @{thms filterlim_split_at eventually_at_left_at_right_imp_at landau_at_top_imp_at
                  asymp_equiv_at_top_imp_at})
       THEN PARALLEL_ALLGOALS tac'
   in
     (preproc_tac ctxt
      THEN' preproc_tac ctxt
      THEN' (SELECT_GOAL at_tac ORELSE' tac'))
     THEN_ALL_NEW (TRY o SELECT_GOAL (SOLVE (HEADGOAL (Simplifier.asm_full_simp_tac ctxt))))
   end
 and tac verbose ctxt = tac' verbose (Inl ctxt)
 
 end
 
 structure Real_Asymp_Basic = Real_Asymp(Multiseries_Expansion_Basic)
diff --git a/src/Pure/conv.ML b/src/Pure/conv.ML
--- a/src/Pure/conv.ML
+++ b/src/Pure/conv.ML
@@ -1,229 +1,237 @@
 (*  Title:      Pure/conv.ML
     Author:     Amine Chaieb, TU Muenchen
     Author:     Sascha Boehme, TU Muenchen
     Author:     Makarius
 
 Conversions: primitive equality reasoning.
 *)
 
 infix 1 then_conv;
 infix 0 else_conv;
 
 signature BASIC_CONV =
 sig
   val then_conv: conv * conv -> conv
   val else_conv: conv * conv -> conv
 end;
 
 signature CONV =
 sig
   include BASIC_CONV
   val no_conv: conv
   val all_conv: conv
   val first_conv: conv list -> conv
   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
   val comb_conv: conv -> conv
   val arg_conv: conv -> conv
   val fun_conv: conv -> conv
   val arg1_conv: conv -> conv
   val fun2_conv: conv -> conv
   val binop_conv: conv -> conv
   val binder_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
   val forall_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
   val implies_conv: conv -> conv -> conv
   val implies_concl_conv: conv -> conv
   val rewr_conv: thm -> conv
   val rewrs_conv: thm list -> conv
   val bottom_rewrs_conv: thm list -> Proof.context -> conv
   val top_rewrs_conv: thm list -> Proof.context -> conv
   val top_sweep_rewrs_conv: thm list -> Proof.context -> conv
   val sub_conv: (Proof.context -> conv) -> Proof.context -> conv
   val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv
   val top_conv: (Proof.context -> conv) -> Proof.context -> conv
   val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv
   val params_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
   val prems_conv: int -> conv -> conv
   val concl_conv: int -> conv -> conv
   val fconv_rule: conv -> thm -> thm
   val gconv_rule: conv -> int -> thm -> thm
 end;
 
 structure Conv: CONV =
 struct
 
 (* basic conversionals *)
 
 fun no_conv _ = raise CTERM ("no conversion", []);
 val all_conv = Thm.reflexive;
 
 fun (cv1 then_conv cv2) ct =
   let
     val eq1 = cv1 ct;
     val eq2 = cv2 (Thm.rhs_of eq1);
   in
     if Thm.is_reflexive eq1 then eq2
     else if Thm.is_reflexive eq2 then eq1
     else Thm.transitive eq1 eq2
   end;
 
 fun (cv1 else_conv cv2) ct =
   (cv1 ct
     handle THM _ => cv2 ct
       | CTERM _ => cv2 ct
       | TERM _ => cv2 ct
       | TYPE _ => cv2 ct);
 
 fun first_conv cvs = fold_rev (curry op else_conv) cvs no_conv;
 fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv;
 
 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;
 
 
 
 (** Pure conversions **)
 
 (* lambda terms *)
 
 fun abs_conv cv ctxt ct =
   (case Thm.term_of ct of
     Abs (a, _, _) =>
       let
         val ((v, ct'), ctxt') = Variable.dest_abs_cterm ct ctxt;
         val eq = cv (v, ctxt') ct';
       in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule a v eq end
   | _ => raise CTERM ("abs_conv", [ct]));
 
 fun combination_conv cv1 cv2 ct =
   let val (ct1, ct2) = Thm.dest_comb ct
   in Thm.combination (cv1 ct1) (cv2 ct2) end;
 
 fun comb_conv cv = combination_conv cv cv;
 fun arg_conv cv = combination_conv all_conv cv;
 fun fun_conv cv = combination_conv cv all_conv;
 
 val arg1_conv = fun_conv o arg_conv;
 val fun2_conv = fun_conv o fun_conv;
 
 fun binop_conv cv = combination_conv (arg_conv cv) cv;
 
 fun binder_conv cv ctxt = arg_conv (abs_conv cv ctxt);
 
 
 (* subterm structure *)
 
 (*cf. SUB_CONV in HOL*)
 fun sub_conv conv ctxt =
   comb_conv (conv ctxt) else_conv
   abs_conv (conv o snd) ctxt else_conv
   all_conv;
 
 (*cf. BOTTOM_CONV in HOL*)
 fun bottom_conv conv ctxt ct =
   (sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct;
 
 (*cf. TOP_CONV in HOL*)
 fun top_conv conv ctxt ct =
   (conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct;
 
 (*cf. TOP_SWEEP_CONV in HOL*)
 fun top_sweep_conv conv ctxt ct =
   (conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct;
 
 
 (* primitive logic *)
 
 fun forall_conv cv ctxt ct =
   (case Thm.term_of ct of
     Const ("Pure.all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct
   | _ => raise CTERM ("forall_conv", [ct]));
 
 fun implies_conv cv1 cv2 ct =
   (case Thm.term_of ct of
     Const ("Pure.imp", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct
   | _ => raise CTERM ("implies_conv", [ct]));
 
 fun implies_concl_conv cv ct =
   (case Thm.term_of ct of
     Const ("Pure.imp", _) $ _ $ _ => arg_conv cv ct
   | _ => raise CTERM ("implies_concl_conv", [ct]));
 
 
 (* rewrite steps *)
 
 (*cf. REWR_CONV in HOL*)
 fun rewr_conv rule ct =
   let
     val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule;
     val lhs = Thm.lhs_of rule1;
     val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
     val rule3 =
       Thm.instantiate (Thm.match (lhs, ct)) rule2
         handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct]);
     val rule4 =
       if Thm.lhs_of rule3 aconvc ct then rule3
       else
         let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3)
         in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (Thm.rhs_of rule3)) end;
   in Thm.transitive rule4 (Thm.beta_conversion true (Thm.rhs_of rule4)) end;
 
 fun rewrs_conv rules = first_conv (map rewr_conv rules);
 
 fun bottom_rewrs_conv rewrs = bottom_conv (K (try_conv (rewrs_conv rewrs)));
 fun top_rewrs_conv rewrs = top_conv (K (try_conv (rewrs_conv rewrs)));
 fun top_sweep_rewrs_conv rewrs = top_sweep_conv (K (rewrs_conv rewrs));
 
 
 (* conversions on HHF rules *)
 
 (*rewrite B in \<And>x1 ... xn. B*)
 fun params_conv n cv ctxt ct =
   if n <> 0 andalso Logic.is_all (Thm.term_of ct)
   then arg_conv (abs_conv (params_conv (n - 1) cv o #2) ctxt) ct
   else cv ctxt ct;
 
 (*rewrite the A's in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
 fun prems_conv 0 _ ct = all_conv ct
   | prems_conv n cv ct =
       (case try Thm.dest_implies ct of
         NONE => all_conv ct
       | SOME (A, B) => Drule.imp_cong_rule (cv A) (prems_conv (n - 1) cv B));
 
 (*rewrite B in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
 fun concl_conv 0 cv ct = cv ct
   | concl_conv n cv ct =
       (case try Thm.dest_implies ct of
         NONE => cv ct
       | SOME (A, B) => Drule.imp_cong_rule (all_conv A) (concl_conv (n - 1) cv B));
 
 
 (* conversions as inference rules *)
 
 (*forward conversion, cf. FCONV_RULE in LCF*)
 fun fconv_rule cv th =
   let val eq = cv (Thm.cprop_of th) in
     if Thm.is_reflexive eq then th
     else Thm.equal_elim eq th
   end;
 
 (*goal conversion*)
 fun gconv_rule cv i th =
   (case try (Thm.cprem_of th) i of
     SOME ct =>
       let val eq = cv ct in
         if Thm.is_reflexive eq then th
         else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th
       end
   | NONE => raise THM ("gconv_rule", i, [th]));
 
 end;
 
 structure Basic_Conv: BASIC_CONV = Conv;
 open Basic_Conv;