--- a/Quot/Prove.thy	Tue Jan 26 20:07:50 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +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, pos)) lthy =
-  let
-    val trm = ML_Context.evaluate lthy true ("r", r) txt
-  in
-    Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy
-  end
-
-  val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source
-in
-  OuterSyntax.local_theory_to_proof "prove" "proving a proposition" 
-    OuterKeyword.thy_goal (parser >> setup_proof)
-end
-*}
-
-end