src/Pure/Tools/codegen_package.ML

         * ((string * CodegenThingol.datatyp) list -> Pretty.T);
 
   val add_pretty_list: string -> string -> string * (int * string)
     -> theory -> theory;
   val add_alias: string * string -> theory -> theory;
-  val set_get_all_datatype_cons : (theory -> (string * string) list)
+  val set_get_all_datatype_cons: (theory -> (string * string) list)
     -> theory -> theory;
-  val set_int_tyco: string -> theory -> theory;
+  val purge_code: theory -> theory;
 
   type appgen;
   val add_appconst: xstring * appgen -> theory -> theory;
   val add_appconst_i: string * appgen -> theory -> theory;
   val appgen_default: appgen;

 val serializers = ref (
   Symtab.empty
   |> Symtab.update (
        #ml CodegenSerializer.serializers
        |> apsnd (fn seri => seri
-            (nsp_dtcon, nsp_class, K false)
+            (nsp_dtcon, nsp_class)
             [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem]]
           )
      )
   |> Symtab.update (
        #haskell CodegenSerializer.serializers

       in CodegenData.put { modl = modl, appgens = appgens,
            target_data = target_data, logic_data = logic_data } thy end;
 
 val print_code = CodegenData.print;
 
+val purge_code = map_codegen_data (fn (_, appgens, target_data, logic_data) => 
+  (empty_module, appgens, target_data, logic_data));
 
 (* advanced name handling *)
 
 fun add_alias (src, dst) =
   map_codegen_data

 (* further theory data accessors *)
 
 fun gen_add_appconst prep_const (raw_c, appgen) thy =
   let
     val c = prep_const thy raw_c;
-    val _ = writeln c;
     val i = (length o fst o strip_type o Sign.the_const_type thy) c
-    val _ = (writeln o string_of_int) i;
   in map_codegen_data
     (fn (modl, appgens, target_data, logic_data) =>
        (modl,
         appgens |> Symtab.update (c, (i, (appgen, stamp ()))),
         target_data, logic_data)) thy

                   val (vars, cos) = (fst o the o CodegenTheorems.get_datatypes thy) dtco
                 in
                   SOME (c, (the o AList.lookup (op =) cos) c ---> Type (dtco, map TFree vars) |> Logic.varifyT)
                 end
             | NONE => NONE;
-
-fun set_int_tyco tyco thy =
-  (serializers := (
-    ! serializers
-    |> Symtab.update (
-         #ml CodegenSerializer.serializers
-         |> apsnd (fn seri => seri
-            (nsp_dtcon, nsp_class, fn tyco' => tyco' = idf_of_name thy nsp_tyco tyco)
-              [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst, nsp_instmem]]
-            )
-       )
-    ); thy);
 
 
 (* definition and expression generators *)
 
 fun check_strict thy f x ((false, _, _), _) =

                 |> ensure_def_class thy tabs supclass
                 ||>> fold_map (exprgen_classlookup thy tabs)
                       (ClassPackage.sortlookup thy ([supclass], arity_typ));
               fun gen_membr (m, ty) trns =
                 trns
-                |> tap (fn _ => writeln ("(1) " ^ m))
                 |> mk_fun thy tabs (m, ty)
-                |> tap (fn _ => writeln "(2)")
                 |-> (fn NONE => error ("could not derive definition for member "
                           ^ quote m ^ " :: " ^ Sign.string_of_typ thy ty)
                       | SOME (funn, sorts) => fold_map (fn (sort, sort_ctxt) =>
                           fold_map (exprgen_classlookup thy tabs)
                             (ClassPackage.sortlookup thy (sort, TFree sort_ctxt)))
                             (print sorts ~~ print operational_arity)
-                #> tap (fn _ => writeln "(3)")
                 #-> (fn lss =>
                        pair (idf_of_name thy nsp_mem m, ((idf_of_name thy nsp_instmem m, funn), lss))));
             in
               trns
               |> debug_msg (fn _ => "trying defgen class instance for (" ^ quote cls

       trns
       |> exprgen_type thy tabs ty
       |-> (fn ty => pair (IVar v))
   | exprgen_term thy tabs (Abs (raw_v, ty, raw_t)) trns =
       let
-        val (v, t) = Term.variant_abs (CodegenThingol.proper_name raw_v, ty, raw_t);
+        val (v, t) = Term.variant_abs (Name.alphanum raw_v, ty, raw_t);
       in
         trns
         |> exprgen_type thy tabs ty
         ||>> exprgen_term thy tabs t
         |-> (fn (ty, e) => pair ((v, ty) `|-> e))

   case Symtab.lookup ((#appgens o CodegenData.get) thy) f
    of SOME (i, (ag, _)) =>
         if length ts < i then
           let
             val tys = Library.take (i - length ts, ((fst o strip_type) ty));
-            val vs = CodegenThingol.give_names [f] tys;
+            val vs = Name.give_names (Name.declare f Name.context) "a" tys;
           in
             trns
             |> fold_map (exprgen_type thy tabs) tys
             ||>> ag thy tabs ((f, ty), ts @ map Free vs)
             |-> (fn (tys, e) => pair (map2 (fn (v, _) => pair v) vs tys `|--> e))

         trns
         |> appgen_default thy tabs app;
 
 fun appgen_case dest_case_expr thy tabs (app as (c_ty, ts)) trns =
   let
-    val _ = (writeln o fst) c_ty;
-    val _ = (writeln o Sign.string_of_typ thy o snd) c_ty;
     val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
     fun clausegen (dt, bt) trns =
       trns
       |> exprgen_term thy tabs dt
       ||>> exprgen_term thy tabs bt;

       else add_alias (src, dst) thy
   in fold add inconsistent thy end;
 
 fun codegen_term t thy =
   thy
-  |> expand_module (SOME (Symtab.keys (#target_data (CodegenData.get thy)))) NONE exprgen_term t;
+  |> expand_module (SOME [] (*(Symtab.keys (#target_data (CodegenData.get thy)))*)) NONE exprgen_term t;
 
 val is_dtcon = has_nsp nsp_dtcon;
 
 fun consts_of_idfs thy =
   map (the o const_of_idf thy (mk_tabs thy NONE));

 fun get_ml_fun_datatype thy resolv =
   let
     val target_data =
       ((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy;
   in
-    CodegenSerializer.ml_fun_datatype (nsp_dtcon, nsp_class, K false)
+    CodegenSerializer.ml_fun_datatype (nsp_dtcon, nsp_class)
       ((Option.map fst oo Symtab.lookup o #syntax_tyco) target_data,
       (Option.map fst oo Symtab.lookup o #syntax_const) target_data)
       resolv
   end;
 

     >> (Toplevel.theory oo fold o fold)
           (fn (target, modifier) => modifier target)
   );
 
 val purgeP =
-  OuterSyntax.command purgeK "purge all defintions for constant" K.thy_decl (
-    Scan.repeat1 P.term
-    >> (Toplevel.theory o purge_consts)
-  );
+  OuterSyntax.command purgeK "purge all incrementally generated code" K.thy_decl
+    (Scan.succeed (Toplevel.theory purge_code));
 
 val aliasP =
   OuterSyntax.command aliasK "declare an alias for a theory identifier" K.thy_decl (
     Scan.repeat1 (P.name -- P.name)
       >> (Toplevel.theory oo fold) add_alias