1.1 --- a/src/Tools/Code/code_target.ML	Wed Dec 23 08:31:14 2009 +0100
     1.2 +++ b/src/Tools/Code/code_target.ML	Wed Dec 23 08:31:15 2009 +0100
     1.3 @@ -356,15 +356,9 @@
     1.4        (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3);
     1.5    in fold (insert (op =)) cs5 cs1 end;
     1.6  
     1.7 -fun cached_program thy = 
     1.8 -  let
     1.9 -    val (naming, program) = Code_Thingol.cached_program thy;
    1.10 -  in (transitivly_non_empty_funs thy naming program, (naming, program)) end
    1.11 -
    1.12  fun export_code thy cs seris =
    1.13    let
    1.14 -    val (cs', (naming, program)) = if null cs then cached_program thy
    1.15 -      else Code_Thingol.consts_program thy cs;
    1.16 +    val (cs', (naming, program)) = Code_Thingol.consts_program thy cs;
    1.17      fun mk_seri_dest dest = case dest
    1.18       of NONE => compile
    1.19        | SOME "-" => export
    1.20 @@ -514,7 +508,7 @@
    1.21  val (inK, module_nameK, fileK) = ("in", "module_name", "file");
    1.22  
    1.23  val code_exprP =
    1.24 -  (Scan.repeat P.term_group
    1.25 +  (Scan.repeat1 P.term_group
    1.26    -- Scan.repeat (P.$$$ inK |-- P.name
    1.27       -- Scan.option (P.$$$ module_nameK |-- P.name)
    1.28       -- Scan.option (P.$$$ fileK |-- P.name)