src/HOL/Hoare/Pointers0.thy

--- a/src/HOL/Hoare/Pointers0.thy	Tue Feb 23 10:11:12 2010 +0100
+++ b/src/HOL/Hoare/Pointers0.thy	Tue Feb 23 10:11:15 2010 +0100
@@ -9,12 +9,12 @@
 - in fact in some case they appear to get (a bit) more complicated.
 *)
 
-theory Pointers0 imports Hoare begin
+theory Pointers0 imports Hoare_Logic begin
 
 subsection "References"
 
-axclass ref < type
-consts Null :: "'a::ref"
+class ref =
+  fixes Null :: 'a
 
 subsection "Field access and update"