diff -r 5983668cac15 -r 852c63072334 src/HOL/ex/Sorting.thy
--- a/src/HOL/ex/Sorting.thy	Fri Mar 10 17:52:48 2000 +0100
+++ b/src/HOL/ex/Sorting.thy	Fri Mar 10 17:53:16 2000 +0100
@@ -6,13 +6,11 @@
 Specification of sorting
 *)
 
-Sorting = List +
+Sorting = Main +
 consts
   sorted1:: [['a,'a] => bool, 'a list] => bool
   sorted :: [['a,'a] => bool, 'a list] => bool
-  mset   :: 'a list => ('a => nat)
-  total  :: (['a,'a] => bool) => bool
-  transf :: (['a,'a] => bool) => bool
+  multiset   :: 'a list => ('a => nat)
 
 primrec
   "sorted1 le [] = True"
@@ -24,10 +22,14 @@
   "sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)"
 
 primrec
-  "mset [] y = 0"
-  "mset (x#xs) y = (if x=y then Suc(mset xs y) else mset xs y)"
+  "multiset [] y = 0"
+  "multiset (x#xs) y = (if x=y then Suc(multiset xs y) else multiset xs y)"
 
-defs
-total_def  "total r == (!x y. r x y | r y x)"
-transf_def "transf f == (!x y z. f x y & f y z --> f x z)"
+constdefs
+  total  :: (['a,'a] => bool) => bool
+   "total r == (ALL x y. r x y | r y x)"
+  
+  transf :: (['a,'a] => bool) => bool
+   "transf f == (ALL x y z. f x y & f y z --> f x z)"
+
 end