--- a/src/HOL/Library/MLString.thy Wed Dec 27 19:09:58 2006 +0100 +++ b/src/HOL/Library/MLString.thy Wed Dec 27 19:09:59 2006 +0100 @@ -74,6 +74,5 @@ (Haskell "_") code_reserved SML string explode -code_reserved Haskell string end