1.1 --- a/src/Tools/Code/code_target.ML	Tue Sep 28 08:38:20 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Tue Sep 28 09:17:33 2010 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4    val add_reserved: string -> string -> theory -> theory
     1.5    val add_include: string -> string * (string * string list) option -> theory -> theory
     1.6  
     1.7 -  val codegen_tool: string (*theory name*) -> bool -> string (*export_code expr*) -> unit
     1.8 +  val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit
     1.9  end;
    1.10  
    1.11  structure Code_Target : CODE_TARGET =
    1.12 @@ -692,10 +692,9 @@
    1.13  
    1.14  (** external entrance point -- for codegen tool **)
    1.15  
    1.16 -fun codegen_tool thyname qnd cmd_expr =
    1.17 +fun codegen_tool thyname cmd_expr =
    1.18    let
    1.19      val thy = Thy_Info.get_theory thyname;
    1.20 -    val _ = quick_and_dirty := qnd;
    1.21      val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
    1.22        (filter Token.is_proper o Outer_Syntax.scan Position.none);
    1.23    in case parse cmd_expr

     2.1 --- a/src/Tools/Code/lib/Tools/codegen	Tue Sep 28 08:38:20 2010 +0200
     2.2 +++ b/src/Tools/Code/lib/Tools/codegen	Tue Sep 28 09:17:33 2010 +0200
     2.3 @@ -55,9 +55,9 @@
     2.4    handle _ => OS.Process.exit OS.Process.failure;"
     2.5  
     2.6  ACTUAL_CMD="val thyname = \"$THYNAME\"; \
     2.7 -  val qnd = $QUICK_AND_DIRTY; \
     2.8 +  val _ = quick_and_dirty := $QUICK_AND_DIRTY; \
     2.9    val cmd_expr = \"$CODE_EXPR\"; \
    2.10 -  val ml_cmd = \"Code_Target.codegen_tool thyname qnd cmd_expr\"; \
    2.11 +  val ml_cmd = \"Code_Target.codegen_tool thyname cmd_expr\"; \
    2.12    $FORMAL_CMD"
    2.13  
    2.14  "$ISABELLE_PROCESS" -r -q -e "$ACTUAL_CMD" "$IMAGE" || exit 1