src/HOLCF/IOA/meta_theory/Simulations.ML
changeset 5132 24f992a25adc
parent 5068 fb28eaa07e01
child 10798 0a1446ff6aff
--- a/src/HOLCF/IOA/meta_theory/Simulations.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Simulations.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -10,7 +10,7 @@
 
 Goal "(A~={}) = (? x. x:A)";
 by (safe_tac set_cs);
-auto();
+by Auto_tac;
 qed"set_non_empty";
 
 Goal "(A Int B ~= {}) = (? x. x: A & x:B)";