# HG changeset patch
# User lcp
# Date 806684554 -7200
# Node ID 026221bc9b2d17db2371589d52eeb428e4e9cf04
# Parent  d3a3cae80f0889cc43c76ea22d757fd31a903cbd
Corrected mixfix declaration of @perm

diff -r d3a3cae80f08 -r 026221bc9b2d src/HOL/ex/Perm.thy
--- a/src/HOL/ex/Perm.thy	Tue Jul 25 17:02:03 1995 +0200
+++ b/src/HOL/ex/Perm.thy	Tue Jul 25 17:02:34 1995 +0200
@@ -9,7 +9,7 @@
 Perm = List +
 
 consts  perm    :: "('a list * 'a list) set"   
-syntax "@perm"  :: "['a list, 'a list] => bool" ("_ <~~> _"  [50] 50)
+syntax "@perm"  :: "['a list, 'a list] => bool" ("_ <~~> _"  [50,50] 50)
 
 translations
     "x <~~> y" == "(x,y) : perm"