reduced prominence of "permissive code generation"

--- a/src/Tools/Code/code_runtime.ML	Thu Jan 30 16:09:03 2014 +0100
+++ b/src/Tools/Code/code_runtime.ML	Thu Jan 30 16:09:04 2014 +0100
@@ -196,7 +196,7 @@
 fun evaluation_code thy module_name tycos consts =
   let
     val ctxt = Proof_Context.init_global thy;
-    val program = Code_Thingol.consts_program thy false consts;
+    val program = Code_Thingol.consts_program thy consts;
     val (ml_modules, target_names) =
       Code_Target.produce_code_for thy
         target NONE module_name [] program (map Constant consts @ map Type_Constructor tycos);

--- a/src/Tools/Code/code_target.ML	Thu Jan 30 16:09:03 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Thu Jan 30 16:09:04 2014 +0100
@@ -8,7 +8,6 @@
 sig
   val cert_tyco: theory -> string -> string
   val read_tyco: theory -> string -> string
-  val read_const_exprs: theory -> string list -> string list
 
   val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
     -> Code_Thingol.program -> Code_Symbol.T list -> unit
@@ -458,44 +457,39 @@
 
 (* code generation *)
 
-fun read_const_exprs thy const_exprs =
-  let
-    val (cs1, cs2) = Code_Thingol.read_const_exprs thy const_exprs;
-    val program = Code_Thingol.consts_program thy true cs2;
-    val cs3 = Code_Thingol.implemented_deps program;
-  in union (op =) cs3 cs1 end;
-
 fun prep_destination "" = NONE
   | prep_destination s = SOME (Path.explode s);
 
 fun export_code thy cs seris =
   let
-    val program = Code_Thingol.consts_program thy false cs;
+    val program = Code_Thingol.consts_program thy cs;
     val _ = map (fn (((target, module_name), some_path), args) =>
       export_code_for thy some_path target NONE module_name args program (map Constant cs)) seris;
   in () end;
 
-fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs)
+fun export_code_cmd raw_cs seris thy = export_code thy
+  (Code_Thingol.read_const_exprs thy raw_cs)
   ((map o apfst o apsnd) prep_destination seris);
 
 fun produce_code thy cs target some_width some_module_name args =
   let
-    val program = Code_Thingol.consts_program thy false cs;
+    val program = Code_Thingol.consts_program thy cs;
   in produce_code_for thy target some_width some_module_name args program (map Constant cs) end;
 
 fun present_code thy cs syms target some_width some_module_name args =
   let
-    val program = Code_Thingol.consts_program thy false cs;
+    val program = Code_Thingol.consts_program thy cs;
   in present_code_for thy target some_width some_module_name args program (map Constant cs, syms) end;
 
 fun check_code thy cs seris =
   let
-    val program = Code_Thingol.consts_program thy false cs;
+    val program = Code_Thingol.consts_program thy cs;
     val _ = map (fn ((target, strict), args) =>
       check_code_for thy target strict args program (map Constant cs)) seris;
   in () end;
 
-fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;
+fun check_code_cmd raw_cs seris thy = check_code thy
+  (Code_Thingol.read_const_exprs thy raw_cs) seris;
 
 local
 

--- a/src/Tools/Code/code_thingol.ML	Thu Jan 30 16:09:03 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML	Thu Jan 30 16:09:04 2014 +0100
@@ -83,8 +83,8 @@
     -> ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list
       * ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list)) list
 
-  val read_const_exprs: theory -> string list -> string list * string list
-  val consts_program: theory -> bool -> string list -> program
+  val read_const_exprs: theory -> string list -> string list
+  val consts_program: theory -> string list -> program
   val dynamic_conv: theory -> (program
     -> ((string * sort) list * typscheme) * iterm -> Code_Symbol.T list -> conv)
     -> conv
@@ -743,19 +743,25 @@
 
 (* program generation *)
 
-fun consts_program thy permissive consts =
+fun consts_program_internal thy permissive consts =
   let
-    fun project program =
-      if permissive then program
-      else Code_Symbol.Graph.restrict
-        (member (op =) (Code_Symbol.Graph.all_succs program
-          (map Constant consts))) program;
     fun generate_consts thy algebra eqngr =
       fold_map (ensure_const thy algebra eqngr permissive);
   in
     invoke_generation permissive thy (Code_Preproc.obtain false thy consts [])
       generate_consts consts
     |> snd
+  end;
+
+fun consts_program_permissive thy = consts_program_internal thy true;
+
+fun consts_program thy consts =
+  let
+    fun project program = Code_Symbol.Graph.restrict
+      (member (op =) (Code_Symbol.Graph.all_succs program
+        (map Constant consts))) program;
+  in
+    consts_program_internal thy false consts
     |> project
   end;
 
@@ -838,9 +844,9 @@
   Code_Preproc.static_value thy postproc consts (lift_evaluator thy evaluator consts);
 
 
-(** diagnostic commands **)
+(** constant expressions **)
 
-fun read_const_exprs thy =
+fun read_const_exprs_internal thy =
   let
     fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
       ((snd o #constants o Consts.dest o Sign.consts_of) thy') [];
@@ -859,6 +865,17 @@
       | NONE => ([Code.read_const thy str], []));
   in pairself flat o split_list o map read_const_expr end;
 
+fun read_const_exprs_all thy = op @ o read_const_exprs_internal thy;
+
+fun read_const_exprs thy const_exprs =
+  let
+    val (consts, consts_permissive) = read_const_exprs_internal thy const_exprs;
+    val consts' = implemented_deps (consts_program_permissive thy consts_permissive);
+  in union (op =) consts' consts end;
+
+
+(** diagnostic commands **)
+
 fun code_depgr thy consts =
   let
     val (_, eqngr) = Code_Preproc.obtain true thy consts [];
@@ -888,8 +905,8 @@
 
 local
 
-fun code_thms_cmd thy = code_thms thy o op @ o read_const_exprs thy;
-fun code_deps_cmd thy = code_deps thy o op @ o read_const_exprs thy;
+fun code_thms_cmd thy = code_thms thy o read_const_exprs_all thy;
+fun code_deps_cmd thy = code_deps thy o read_const_exprs_all thy;
 
 in