1.1 --- a/src/HOL/Library/Array.thy	Tue Jul 29 14:07:23 2008 +0200
     1.2 +++ b/src/HOL/Library/Array.thy	Tue Jul 29 14:20:22 2008 +0200
     1.3 @@ -198,7 +198,7 @@
     1.4  
     1.5  subsubsection {* Haskell *}
     1.6  
     1.7 -code_type array (Haskell "STArray '_s _")
     1.8 +code_type array (Haskell "STArray/ RealWorld/ _")
     1.9  code_const Array (Haskell "error/ \"bare Array\"")
    1.10  code_const Array.new' (Haskell "newArray/ (0,/ _)")
    1.11  code_const Array.of_list' (Haskell "newListArray/ (0,/ _)")

     2.1 --- a/src/HOL/Library/Heap_Monad.thy	Tue Jul 29 14:07:23 2008 +0200
     2.2 +++ b/src/HOL/Library/Heap_Monad.thy	Tue Jul 29 14:20:22 2008 +0200
     2.3 @@ -169,14 +169,6 @@
     2.4  in [(@{const_syntax "run"}, tr')] end;
     2.5  *}
     2.6  
     2.7 -subsubsection {* Plain evaluation *}
     2.8 -
     2.9 -definition
    2.10 -  evaluate :: "'a Heap \<Rightarrow> 'a"
    2.11 -where
    2.12 -  [code del]: "evaluate f = (case execute f Heap.empty
    2.13 -    of (Inl x, _) \<Rightarrow> x)"
    2.14 -
    2.15  
    2.16  subsection {* Monad properties *}
    2.17  
    2.18 @@ -330,6 +322,7 @@
    2.19  import qualified Data.STRef;
    2.20  import qualified Data.Array.ST;
    2.21  
    2.22 +type RealWorld = Control.Monad.ST.RealWorld;
    2.23  type ST s a = Control.Monad.ST.ST s a;
    2.24  type STRef s a = Data.STRef.STRef s a;
    2.25  type STArray s a = Data.Array.ST.STArray s Int a;
    2.26 @@ -356,16 +349,15 @@
    2.27  writeArray :: STArray s a -> Int -> a -> ST s ();
    2.28  writeArray = Data.Array.ST.writeArray;*}
    2.29  
    2.30 -code_reserved Haskell ST STRef Array
    2.31 +code_reserved Haskell RealWorld ST STRef Array
    2.32    runST
    2.33    newSTRef reasSTRef writeSTRef
    2.34    newArray newListArray lengthArray readArray writeArray
    2.35  
    2.36  text {* Monad *}
    2.37  
    2.38 -code_type Heap (Haskell "ST '_s _")
    2.39 -code_const Heap (Haskell "error \"bare Heap\")")
    2.40 -code_const evaluate (Haskell "runST")
    2.41 +code_type Heap (Haskell "ST/ RealWorld/ _")
    2.42 +code_const Heap (Haskell "error/ \"bare Heap\"")
    2.43  code_monad run "op \<guillemotright>=" Haskell
    2.44  code_const return (Haskell "return")
    2.45  code_const "Heap_Monad.Fail" (Haskell "_")

     3.1 --- a/src/HOL/Library/Ref.thy	Tue Jul 29 14:07:23 2008 +0200
     3.2 +++ b/src/HOL/Library/Ref.thy	Tue Jul 29 14:20:22 2008 +0200
     3.3 @@ -82,7 +82,7 @@
     3.4  
     3.5  subsubsection {* Haskell *}
     3.6  
     3.7 -code_type ref (Haskell "STRef '_s _")
     3.8 +code_type ref (Haskell "STRef/ RealWorld/ _")
     3.9  code_const Ref (Haskell "error/ \"bare Ref\"")
    3.10  code_const Ref.new (Haskell "newSTRef")
    3.11  code_const Ref.lookup (Haskell "readSTRef")