--- a/src/HOL/Imperative_HOL/Ref.thy Tue Sep 21 15:46:06 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Wed Sep 22 09:40:11 2010 +0200
@@ -273,15 +273,17 @@
by (simp add: ref'_def)
-text {* SML *}
+text {* SML / Eval *}
-code_type ref (SML "_/ Unsynchronized.ref")
+code_type ref (SML "_/ ref")
+code_type ref (Eval "_/ Unsynchronized.ref")
code_const Ref (SML "raise/ (Fail/ \"bare Ref\")")
-code_const ref' (SML "(fn/ ()/ =>/ Unsynchronized.ref/ _)")
+code_const ref' (SML "(fn/ ()/ =>/ ref/ _)")
+code_const ref' (Eval "(fn/ ()/ =>/ Unsynchronized.ref/ _)")
code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)")
code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)")
-code_reserved SML Unsynchronized
+code_reserved Eval Unsynchronized
text {* OCaml *}