# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272641503 -3600
# Node ID 233bb805a4df2875cfe4e7f872eea21ab6ea9b45
# Parent  b96e8cf868917d9d6408e0ceacae7ed05ebca6fa
replaced hide by the new hide_const

diff -r b96e8cf86891 -r 233bb805a4df Pearl-jv/Paper.thy
--- a/Pearl-jv/Paper.thy	Fri Apr 30 15:36:02 2010 +0100
+++ b/Pearl-jv/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"
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"