--- a/src/HOLCF/explicit_domains/Dagstuhl.ML Mon Jan 29 14:16:13 1996 +0100
+++ b/src/HOLCF/explicit_domains/Dagstuhl.ML Tue Jan 30 13:42:57 1996 +0100
@@ -7,7 +7,7 @@
val prems = goal Dagstuhl.thy "YYS << scons`y`YYS";
-by (rewrite_goals_tac [YYS_def]);
+by (rewtac YYS_def);
by (rtac fix_ind 1);
by (resolve_tac adm_thms 1);
by (cont_tacR 1);
@@ -52,7 +52,7 @@
(* ------------------------------------------------------------------------ *)
val prems = goal Dagstuhl.thy "YYS << YS";
-by (rewrite_goals_tac [YYS_def]);
+by (rewtac YYS_def);
by (rtac fix_least 1);
by (rtac (beta_cfun RS ssubst) 1);
by (cont_tacR 1);
@@ -60,7 +60,7 @@
val lemma6=result();
val prems = goal Dagstuhl.thy "YS << YYS";
-by (rewrite_goals_tac [YS_def]);
+by (rewtac YS_def);
by (rtac fix_ind 1);
by (resolve_tac adm_thms 1);
by (cont_tacR 1);