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