--- a/Attic/Prove.thy	Fri May 21 10:47:45 2010 +0200
+++ b/Attic/Prove.thy	Fri May 21 11:46:47 2010 +0200
@@ -9,19 +9,18 @@
 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 =
+    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 = SpecParse.opt_thm_name ":" -- OuterParse.ML_source
+  val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
 in
-  OuterSyntax.local_theory_to_proof "prove" "proving a proposition" 
-    OuterKeyword.thy_goal (parser >> setup_proof)
+  Outer_Syntax.local_theory_to_proof "prove" "proving a proposition" 
+    Keyword.thy_goal (parser >> setup_proof)
 end
 *}