optionally ignore errors during translation of equations

--- a/src/Tools/Code/code_eval.ML	Wed Apr 21 12:11:48 2010 +0200
+++ b/src/Tools/Code/code_eval.ML	Wed Apr 21 15:20:57 2010 +0200
@@ -25,7 +25,7 @@
 
 fun evaluation_code thy tycos consts =
   let
-    val (consts', (naming, program)) = Code_Thingol.consts_program thy consts;
+    val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
     val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
     val (ml_code, target_names) = Code_ML.evaluation_code_of thy target
       eval_struct_name naming program (consts' @ tycos');

--- a/src/Tools/Code/code_target.ML	Wed Apr 21 12:11:48 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Wed Apr 21 15:20:57 2010 +0200
@@ -329,7 +329,7 @@
 
 fun code_of thy target some_width module_name cs names_stmt =
   let
-    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy cs;
+    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
   in
     string (names_stmt naming)
       (serialize thy target some_width (SOME module_name) [] naming program names_cs)
@@ -347,15 +347,15 @@
 fun read_const_exprs thy cs =
   let
     val (cs1, cs2) = Code_Thingol.read_const_exprs thy cs;
-    val (names3, (naming, program)) = Code_Thingol.consts_program thy cs2;
-    val names4 = transitivly_non_empty_funs thy naming program;
-    val cs5 = map_filter
-      (fn (c, name) => if member (op =) names4 name then SOME c else NONE) (cs2 ~~ names3);
-  in fold (insert (op =)) cs5 cs1 end;
+    val (names2, (naming, program)) = Code_Thingol.consts_program thy true cs2;
+    val names3 = transitivly_non_empty_funs thy naming program;
+    val cs3 = map_filter (fn (c, name) =>
+      if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
+  in union (op =) cs3 cs1 end;
 
 fun export_code thy cs seris =
   let
-    val (cs', (naming, program)) = Code_Thingol.consts_program thy cs;
+    val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;
     fun mk_seri_dest dest = case dest
      of NONE => compile
       | SOME "-" => export