--- a/src/HOL/Quot/FRACT.thy	Fri Apr 25 15:31:51 1997 +0200
+++ b/src/HOL/Quot/FRACT.thy	Fri Apr 25 15:33:19 1997 +0200
@@ -9,7 +9,7 @@
 FRACT = NPAIR + HQUOT +
 instance 
 	NP::per	
-	{| (etac per_sym_NP 1) THEN (etac per_trans_NP 1) THEN (atac 1) |}
+	{| (etac per_trans_NP 1) THEN (atac 1) THEN (etac per_sym_NP 1) |}
 
 (* now define fractions *)
 
@@ -20,4 +20,4 @@
 	half ::	"fract"
 
 defs    half_def    "half == <[abs_NP(1,2)]>"
-end
\ No newline at end of file
+end