--- a/Attic/Prove.thy	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-theory Prove
-imports Plain 
-begin
-
-ML {*
-val r = Unsynchronized.ref (NONE:(unit -> term) option)
-*}
-
-ML {*
-let
-  fun after_qed thm_name thms lthy =
-    Local_Theory.note (thm_name, (flat thms)) lthy |> snd
-  fun setup_proof (name_spec, (txt, _)) lthy =
-  let
-    val trm = ML_Context.evaluate lthy true ("r", r) txt
-  in
-    Proof.theorem NONE (after_qed name_spec) [[(trm,[])]] lthy
-  end
-
-  val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
-in
-  Outer_Syntax.local_theory_to_proof "prove" "proving a proposition" 
-    Keyword.thy_goal (parser >> setup_proof)
-end
-*}
-
-end