src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML

     | Free _ =>
       Subgoal.FOCUS_PREMS (fn {context, params = params, prems, asms, concl, schematics} =>
         let
           val prems' = maps dest_conjunct_prem (take nargs prems)
         in
-          Simplifier.rewrite_goal_tac
-            (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+          rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
         end) ctxt 1
     | Abs _ => raise Fail "prove_param: No valid parameter term"
   in
     REPEAT_DETERM (rtac @{thm ext} 1)
     THEN print_tac options "prove_param"

              THEN asm_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
              THEN TRY (
                 let
                   val prems' = maps dest_conjunct_prem (take nargs prems)
                 in
-                  Simplifier.rewrite_goal_tac
+                  rewrite_goal_tac
                     (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
                 end
              THEN REPEAT_DETERM (rtac @{thm refl} 1))
              THEN print_tac options "after if simp; in SUBPROOF") ctxt 1))))
     THEN print_tac options "after if simplification"

       THEN Subgoal.FOCUS_PREMS
              (fn {context, params, prems, asms, concl, schematics} =>
               let
                 val prems' = maps dest_conjunct_prem (take nargs prems)
               in
-                Simplifier.rewrite_goal_tac
-                  (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
+                rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
               end) ctxt 1
       THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
     | prove_prems out_ts ((p, deriv) :: ps) =
       let
         val premposition = (find_index (equal p) clauses) + nargs