diff -r b96e8cf86891 -r 233bb805a4df Pearl/Paper.thy
--- a/Pearl/Paper.thy	Fri Apr 30 15:36:02 2010 +0100
+++ b/Pearl/Paper.thy	Fri Apr 30 16:31:43 2010 +0100
@@ -30,7 +30,7 @@
 *)
 
 (* sort is used in Lists for sorting *)
-hide const sort
+hide_const sort
 
 abbreviation
   "sort \<equiv> sort_of"