src/HOL/Quot/NPAIR.ML

--- a/src/HOL/Quot/NPAIR.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Quot/NPAIR.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -7,13 +7,13 @@
 open NPAIR;
 
 goalw thy [rep_NP_def] "rep_NP(abs_NP np) = np";
-auto();
+by (Auto_tac());
 qed "rep_abs_NP";
 
 Addsimps [rep_abs_NP];
 
 val prems = goalw thy [per_NP_def] "eqv (x::NP) y ==> eqv y x";
 by (cut_facts_tac prems 1);
-auto();
+by (Auto_tac());
 qed "per_sym_NP";