--- a/ProgTutorial/Helper/Command/Command.thy	Sat Aug 28 13:37:25 2010 +0800
+++ b/ProgTutorial/Helper/Command/Command.thy	Fri Oct 29 11:00:37 2010 +0100
@@ -40,8 +40,13 @@
 *}
 
 ML {*
-val r = Unsynchronized.ref (NONE:(unit -> term) option)
+structure Result = Proof_Data(
+  type T = unit -> term
+  fun init thy () = error "Result")
+
+val result_cookie = (Result.get, Result.put, "Result.put")
 *}
+
 ML{*
 let
    fun after_qed thm_name thms lthy =
@@ -49,7 +54,7 @@
 
    fun setup_proof (thm_name, (txt, pos)) lthy =
    let
-     val trm = ML_Context.evaluate lthy true ("r", r) txt
+     val trm = Code_Runtime.value lthy result_cookie ("", txt)
    in
      Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy
    end
@@ -63,4 +68,5 @@
 
 
 
+
 end