src/Pure/Thy/thy_output.ML

--- a/src/Pure/Thy/thy_output.ML	Sun Apr 25 15:13:33 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sun Apr 25 15:52:03 2010 +0200
@@ -574,7 +574,7 @@
       val prop_src =
         (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
       val _ = context
-        |> Proof.theorem_i NONE (K I) [[(prop, [])]]
+        |> Proof.theorem NONE (K I) [[(prop, [])]]
         |> Proof.global_terminal_proof methods;
     in output (maybe_pretty_source (pretty_term context) prop_src [prop]) end);