src/HOL/Quot/NPAIR.ML

--- a/src/HOL/Quot/NPAIR.ML	Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Quot/NPAIR.ML	Wed Dec 24 10:02:30 1997 +0100
@@ -7,13 +7,13 @@
 open NPAIR;
 
 goalw thy [rep_NP_def] "rep_NP(abs_NP np) = np";
-by (Auto_tac());
+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);
-by (Auto_tac());
+by Auto_tac;
 qed "per_sym_NP";