--- a/ProgTutorial/Parsing.thy	Sat Aug 28 13:37:25 2010 +0800
+++ b/ProgTutorial/Parsing.thy	Fri Oct 29 11:00:37 2010 +0100
@@ -802,6 +802,7 @@
   for inductive predicates of the form:
 *}
 
+
 simple_inductive
   even and odd
 where
@@ -809,7 +810,6 @@
 | evenS: "odd n \<Longrightarrow> even (Suc n)"
 | oddS: "even n \<Longrightarrow> odd (Suc n)"
 
-
 text {*
   For this we are going to use the parser:
 *}
@@ -1202,27 +1202,37 @@
   
 *}
 
-ML_val{*val r = Unsynchronized.ref (NONE:(unit -> term) option)*}
+ML {*
+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 =
         Local_Theory.note (thm_name, (flat thms)) lthy |> snd
 
    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
 
    val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
+ 
 in
    Outer_Syntax.local_theory_to_proof "foobar_prove" "proving a proposition" 
      Keyword.thy_goal (parser >> setup_proof)
 end*}
 
+(*
 foobar_prove test: {* @{prop "True"} *}
 apply(rule TrueI)
 done
+*)
 
 (*
 ML {*