diff -r 5b33e732e459 -r 42e6b8502d52 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Nov 07 17:52:12 2000 +0100
+++ b/src/Pure/Isar/method.ML	Tue Nov 07 17:53:12 2000 +0100
@@ -279,7 +279,7 @@
 (* atomize meta-connectives *)
 
 fun rewrite_goal_tac rews =
-  Tactic.asm_rewrite_goal_tac (true, false, false) (K no_tac) (Thm.mss_of 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