src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 31205 98370b26c2ce
parent 31058 9f151b096533
child 31724 9b5a128cdb5c
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue May 19 13:57:51 2009 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue May 19 16:54:55 2009 +0200
     1.3 @@ -274,7 +274,7 @@
     1.4  subsubsection {* Logical intermediate layer *}
     1.5  
     1.6  definition
     1.7 -  Fail :: "message_string \<Rightarrow> exception"
     1.8 +  Fail :: "String.literal \<Rightarrow> exception"
     1.9  where
    1.10    [code del]: "Fail s = Exn"
    1.11