src/HOL/Quot/NPAIR.thy

--- a/src/HOL/Quot/NPAIR.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Quot/NPAIR.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -18,7 +18,7 @@
 
 (* NPAIR (continued) *)
 defs	per_NP_def 
-  "eqv ==(%x y.fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"
+  "eqv ==(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"
 
 (* for proves of this rule see [Slo97diss] *)
 rules