diff -r 2f5686cf8c9a -r ab03cfd6be3a src/HOL/Lfp.ML
--- a/src/HOL/Lfp.ML	Sat Sep 23 16:11:38 2000 +0200
+++ b/src/HOL/Lfp.ML	Sat Sep 23 16:12:07 2000 +0200
@@ -55,9 +55,8 @@
 
 (** Definition forms of lfp_Tarski and induct, to control unfolding **)
 
-val [rew,mono] = goal (the_context ()) "[| h==lfp(f);  mono(f) |] ==> h = f(h)";
-by (rewtac rew);
-by (rtac (mono RS lfp_Tarski) 1);
+Goal "[| h==lfp(f);  mono(f) |] ==> h = f(h)";
+by (auto_tac (claset() addSIs [lfp_Tarski], simpset()));  
 qed "def_lfp_Tarski";
 
 val rew::prems = Goal