src/Tools/Code/code_target.ML
changeset 37898 eb89d0ac75fb
parent 37881 096c8397c989
parent 37863 7f113caabcf4
child 37972 f37a8d488105
     1.1 --- a/src/Tools/Code/code_target.ML	Wed Jul 21 09:46:36 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Wed Jul 21 16:50:42 2010 +0200
     1.3 @@ -603,7 +603,7 @@
     1.4  fun shell_command thyname cmd = Toplevel.program (fn _ =>
     1.5    (use_thy thyname; case Scan.read Token.stopper (Parse.!!! code_exprP)
     1.6      ((filter Token.is_proper o Outer_Syntax.scan Position.none) cmd)
     1.7 -   of SOME f => (writeln "Now generating code..."; f (theory thyname))
     1.8 +   of SOME f => (writeln "Now generating code..."; f (Thy_Info.get_theory thyname))
     1.9      | NONE => error ("Bad directive " ^ quote cmd)))
    1.10    handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
    1.11