src/Tools/Code/code_target.ML

     Keyword.diag (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
 
 fun shell_command thyname cmd = Toplevel.program (fn _ =>
   (use_thy thyname; case Scan.read Token.stopper (Parse.!!! code_exprP)
     ((filter Token.is_proper o Outer_Syntax.scan Position.none) cmd)
-   of SOME f => (writeln "Now generating code..."; f (theory thyname))
+   of SOME f => (writeln "Now generating code..."; f (Thy_Info.get_theory thyname))
     | NONE => error ("Bad directive " ^ quote cmd)))
   handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
 
 end; (*local*)