# HG changeset patch
# User wenzelm
# Date 1207826661 -7200
# Node ID 3f757f8acf440b79d254081944d76cdc70826192
# Parent  410d02ea13c9853d89d8ac92a1e1dfec0bdb5886
replaced Isar.toplevel by Toplevel.program;

diff -r 410d02ea13c9 -r 3f757f8acf44 src/Tools/code/code_package.ML
--- a/src/Tools/code/code_package.ML	Thu Apr 10 13:24:20 2008 +0200
+++ b/src/Tools/code/code_package.ML	Thu Apr 10 13:24:21 2008 +0200
@@ -275,7 +275,7 @@
   OuterSyntax.command codeK "generate executable code for constants"
     K.diag (P.!!! (code_exprP code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
 
-fun codegen_shell_command thyname cmd = Isar.toplevel (fn _ =>
+fun codegen_shell_command thyname cmd = Toplevel.program (fn _ =>
   (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd)
    of SOME f => (writeln "Now generating code..."; f (theory thyname))
     | NONE => error ("Bad directive " ^ quote cmd)))