--- a/src/Pure/Isar/method.ML Fri Nov 10 19:12:30 2000 +0100
+++ b/src/Pure/Isar/method.ML Fri Nov 10 19:13:01 2000 +0100
@@ -39,7 +39,6 @@
val insert_facts: Proof.method
val unfold: thm list -> Proof.method
val fold: thm list -> Proof.method
- val rewrite_goal_tac: thm list -> int -> tactic
val atomize_tac: thm list -> int -> tactic
val atomize_goal: thm list -> int -> thm -> thm
val multi_resolve: thm list -> thm -> thm Seq.seq
@@ -278,9 +277,6 @@
(* atomize meta-connectives *)
-fun rewrite_goal_tac rews =
- Tactic.asm_rewrite_goal_tac (true, false, false) (K no_tac) (MetaSimplifier.mss_of rews);
-
fun atomize_tac rews =
let val rew_tac = rewrite_goal_tac rews in
fn i => fn thm =>