diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Fri Apr 16 20:56:40 2010 +0200 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Fri Apr 16 21:28:09 2010 +0200 @@ -8,7 +8,7 @@ imports "~~/src/HOL/Imperative_HOL/Imperative_HOL" Subarray begin -hide (open) const swap rev +hide_const (open) swap rev fun swap :: "'a\heap array \ nat \ nat \ unit Heap" where "swap a i j = (do