src/Provers/induct_method.ML

   MetaSimplifier.rewrite_term thy Data.atomize []
   #> ObjectLogic.drop_judgment thy;
 
 val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
 
-val atomize_tac = Goal.rewrite_goal_tac Data.atomize;
+val atomize_tac = Simplifier.rewrite_goal_tac Data.atomize;
 
 val inner_atomize_tac =
-  Goal.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
+  Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
 
 
 (* rulify *)
 
 fun rulify_term thy =

     val rulify = rulify_term thy;
     val (As, B) = Logic.strip_horn (Thm.prop_of thm);
   in (thy, Logic.list_implies (map rulify As, rulify B)) end;
 
 val rulify_tac =
-  Goal.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
-  Goal.rewrite_goal_tac Data.rulify_fallback THEN'
+  Simplifier.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
+  Simplifier.rewrite_goal_tac Data.rulify_fallback THEN'
   Goal.conjunction_tac THEN_ALL_NEW
-  (Goal.rewrite_goal_tac [conjunction_imp] THEN' Goal.norm_hhf_tac);
+  (Simplifier.rewrite_goal_tac [conjunction_imp] THEN' Goal.norm_hhf_tac);
 
 
 (* prepare rule *)
 
 fun rule_instance thy inst rule =

       SOME concl =>
         (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN' rtac asm_rl) i
     | NONE => all_tac)
   end);
 
-fun miniscope_tac p i = PRIMITIVE (Conv.fconv_rule
-  (Conv.goals_conv (Library.equal i)
-    (Conv.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]))));
+fun miniscope_tac p =
+  CONVERSION (Conv.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]));
 
 in
 
 fun fix_tac _ _ [] = K all_tac
   | fix_tac ctxt n xs = SUBGOAL (fn (goal, i) =>