--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys2/MLs.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -0,0 +1,61 @@
+theory MLs
+imports Pure
+keywords "ML_psf" :: prf_script and
+         "ML_goal" :: thy_goal
+begin
+
+section {* ML for proof state transformation *}
+
+ML {*
+  structure ML_psf = Proof_Data (
+    type T = Proof.state -> Proof.state
+    fun init _ = undefined
+  )
+*}
+
+
+ML {*
+ fun ml_psf (txt, pos) state =   
+        (((Proof.context_of state) |>
+         Context.proof_map (ML_Context.expression Position.none 
+                 "val psf : Proof.state -> Proof.state"
+                  "Context.map_proof (ML_psf.put psf)"  (ML_Lex.read pos txt)) |>
+         ML_psf.get) state):Proof.state
+*}
+
+ML {*
+val _ =
+  Outer_Syntax.command @{command_spec "ML_psf"} "ML state transfer function"
+    (Parse.ML_source >> (Toplevel.print oo (Toplevel.proof o ml_psf)))
+*}
+
+section {* ML for global goal establishment *}
+
+ML {*
+  structure ML_goal = Proof_Data (
+    type T = local_theory -> Proof.state
+    fun init _ = undefined
+  )
+*}
+
+ML {*
+ fun ml_goal (txt, pos) ctxt =   
+        ((ctxt |>
+         Context.proof_map (ML_Context.expression Position.none 
+                 "val goalf : local_theory -> Proof.state"
+                  "Context.map_proof (ML_goal.put goalf)"  (ML_Lex.read pos txt)) |>
+         ML_goal.get) ctxt) :Proof.state
+*}
+
+ML {*
+val _ =
+  Outer_Syntax.local_theory_to_proof @{command_spec "ML_goal"} "ML goal function"
+    (Parse.ML_source >> ml_goal)
+*}
+
+ML {*
+  fun start_theorem prop = Proof.theorem NONE (K I) [[(prop, [])]]
+*}
+
+end
+