# HG changeset patch
# User haftmann
# Date 1285141211 -7200
# Node ID 564448a92ae03c6159d966cbe810fbe02e7fe747
# Parent  7af0441a3a477c9abf7e21e0612ac4ec760d3385
distinguish SML and Eval explicitly

diff -r 7af0441a3a47 -r 564448a92ae0 src/HOL/Imperative_HOL/Ref.thy
--- 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 *}