diff -r 75873e94357c -r 1c4672d130b1 src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Wed Jul 11 11:27:46 2007 +0200
+++ b/src/HOL/Library/Permutation.thy	Wed Jul 11 11:28:13 2007 +0200
@@ -8,19 +8,13 @@
 imports Multiset
 begin
 
-consts
-  perm :: "('a list * 'a list) set"
-
-abbreviation
-  perm_rel :: "'a list => 'a list => bool"  ("_ <~~> _"  [50, 50] 50) where
-  "x <~~> y == (x, y) \<in> perm"
-
-inductive perm
-  intros
+inductive
+  perm :: "'a list => 'a list => bool"  ("_ <~~> _"  [50, 50] 50)
+  where
     Nil  [intro!]: "[] <~~> []"
-    swap [intro!]: "y # x # l <~~> x # y # l"
-    Cons [intro!]: "xs <~~> ys ==> z # xs <~~> z # ys"
-    trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs"
+  | swap [intro!]: "y # x # l <~~> x # y # l"
+  | Cons [intro!]: "xs <~~> ys ==> z # xs <~~> z # ys"
+  | trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs"
 
 lemma perm_refl [iff]: "l <~~> l"
   by (induct l) auto