--- a/Attic/Prove.thy	Sun Apr 25 09:26:36 2010 +0200
+++ b/Attic/Prove.thy	Mon Apr 26 08:08:20 2010 +0200
@@ -15,7 +15,7 @@
   let
     val trm = ML_Context.evaluate lthy true ("r", r) txt
   in
-    Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy
+    Proof.theorem NONE (after_qed name_spec) [[(trm,[])]] lthy
   end
 
   val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source