src/Pure/Thy/thy_output.ML
changeset 36323 655e2d74de3a
parent 36163 823c9400eb62
child 36446 06081e4921d6
     1.1 --- a/src/Pure/Thy/thy_output.ML	Sun Apr 25 15:13:33 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Apr 25 15:52:03 2010 +0200
     1.3 @@ -574,7 +574,7 @@
     1.4        val prop_src =
     1.5          (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
     1.6        val _ = context
     1.7 -        |> Proof.theorem_i NONE (K I) [[(prop, [])]]
     1.8 +        |> Proof.theorem NONE (K I) [[(prop, [])]]
     1.9          |> Proof.global_terminal_proof methods;
    1.10      in output (maybe_pretty_source (pretty_term context) prop_src [prop]) end);
    1.11