src/Pure/Tools/codegen_package.ML

     -> theory -> theory;
   val set_get_datatype: (theory -> string -> ((string * sort) list * (string * typ list) list) option)
     -> theory -> theory;
   val set_int_tyco: string -> theory -> theory;
 
-  val codegen_incr: term -> theory -> (CodegenThingol.iexpr * (string * CodegenThingol.def) list) * theory;
+  val codegen_term: term -> theory -> CodegenThingol.iexpr * theory;
   val is_dtcon: string -> bool;
-  val consts_of_idfs: theory -> string list -> (string * (string * typ)) list
-
+  val consts_of_idfs: theory -> string list -> (string * typ) list;
+  val idfs_of_consts: theory -> (string * typ) list -> string list;
+  val get_root_module: theory -> CodegenThingol.module;
   val get_ml_fun_datatype: theory -> (string -> string)
     -> ((string * CodegenThingol.funn) list -> Pretty.T)
         * ((string * CodegenThingol.datatyp) list -> Pretty.T);
 
   val appgen_default: appgen;

       |> cons c''
       |> space_implode "_"
       |> curry (op ^ o swap) ((implode oo replicate) i "'")
     end;
   fun is_valid _ _ = true;
-  fun maybe_unique thy (c, ty) = 
+  fun maybe_unique thy (c, ty) =
     if is_overloaded thy c
       then NONE
       else (SOME o idf_of_name thy nsp_const) c;
   fun re_mangle thy idf =
    case name_of_idf thy nsp_const idf

     (fn (modl, gens, target_data, logic_data) =>
        (modl,
         gens |> map_gens
           (fn (appconst, eqextrs) =>
             (appconst, eqextrs
-             |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name)
+    |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name)
                  (name, (eqx, stamp ())))),
              target_data, logic_data));
 
 fun get_eqextrs thy tabs =
   (map (fn (name, (eqx, _)) => (name, eqx thy tabs)) o #eqextrs o #gens o CodegenData.get) thy;

 and exprgen_type thy tabs (TVar _) trns =
       error "TVar encountered during code generation"
   | exprgen_type thy tabs (TFree v_s) trns =
       trns
       |> exprgen_tyvar_sort thy tabs v_s
-      |-> (fn v_s => pair (IVarT v_s))
+      |-> (fn (v, sort) => pair (IVarT v))
   | exprgen_type thy tabs (Type ("fun", [t1, t2])) trns =
       trns
       |> exprgen_type thy tabs t1
       ||>> exprgen_type thy tabs t2
       |-> (fn (t1', t2') => pair (t1' `-> t2'))

     ||>> exprgen_term thy tabs t_body
     |-> (fn ((e, abs), body) => pair (ICase (e, [(abs, body)])))
   end;
 
 fun appgen_split strip_abs thy tabs (c, [t2]) trns =
-  let
-    val ([p], body) = strip_abs 1 (Const c $ t2)
-  in
-    trns
-    |> exprgen_term thy tabs p
-    ||>> exprgen_term thy tabs body
-    |-> (fn (e, body) => pair (e `|-> body))
-  end;
+  case strip_abs 1 (Const c $ t2)
+   of ([p], body) =>
+        trns
+        |> exprgen_term thy tabs p
+        ||>> exprgen_term thy tabs body
+        |-> (fn (e, body) => pair (e `|-> body))
+    | _ =>
+        trns
+        |> appgen_default thy tabs (c, [t2]);
 
 fun appgen_number_of mk_int_to_nat bin_to_int tyco_int tyco_nat thy tabs ((_,
   Type (_, [_, ty as Type (tyco, [])])), [bin]) trns =
     if tyco = tyco_int then
       trns

             end) ((#2 o #constants o Consts.dest o #consts o Sign.rep_sg) thy)
       |> (fn (overltab1, overltab2) =>
             let
               val c = "op =";
               val ty = Sign.the_const_type thy c;
-              fun inst dtco = 
+              fun inst dtco =
                 map_atyps (fn _ => Type (dtco,
                   (map (fn (v, sort) => TVar ((v, 0), sort)) o fst o the o get_datatype thy) dtco)) ty
               val dtcos = fold (insert (op =) o snd) (get_all_datatype_cons thy) [];
               val tys = map inst dtcos;
             in

                 val key = ((NameSpace.drop_base o NameSpace.drop_base) co, NameSpace.base co);
               in AList.default (op =) (key, []) #> AList.map_entry (op =) key (cons (co, dtco)) end
             ) (get_all_datatype_cons thy) [])
       |-> (fn _ => I);
     fun mk_clsmemtab thy =
-      Symtab.empty
+   Symtab.empty
       |> Symtab.fold
           (fn (class, (clsmems, _)) => fold
             (fn clsmem => Symtab.update (clsmem, class)) clsmems)
               (ClassPackage.get_classtab thy);
     val deftab = extract_defs thy;

         add_case_const_i get_case_const_data case_c thy;
   in
     fold ensure (get_datatype_case_consts thy) thy
   end;
 
-fun codegen_incr t thy =
+fun codegen_term t thy =
   thy
-  |> `(#modl o CodegenData.get)
-  ||>> expand_module NONE exprsgen_term [t]
-  ||>> `(#modl o CodegenData.get)
-  |-> (fn ((modl_old, [t]), modl_new) => pair (t, CodegenThingol.diff_module (modl_new, modl_old)));
+  |> expand_module NONE exprsgen_term [t]
+  |-> (fn [t] => pair t);
 
 val is_dtcon = has_nsp nsp_dtcon;
 
 fun consts_of_idfs thy =
-  let
-    val tabs = mk_tabs thy;
-  in
-    map (fn idf => (idf, (the o recconst_of_idf thy tabs) idf))
-  end;
+  map (the o recconst_of_idf thy (mk_tabs thy));
+
+fun idfs_of_consts thy =
+  map (idf_of_const thy (mk_tabs thy));
+
+val get_root_module = (#modl o CodegenData.get);
 
 fun get_ml_fun_datatype thy resolv =
   let
-    val target_data = 
+    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)
       ((Option.map fst oo Symtab.lookup o #syntax_tyco) target_data,
       (Option.map fst oo Symtab.lookup o #syntax_const) target_data)

 
 
 (** toplevel interface **)
 
 local
- 
+
 fun generate_code (SOME raw_consts) thy =
-      let
+   let
         val consts = map (read_const thy) raw_consts;
       in
         thy
         |> expand_module NONE (fold_map oo ensure_def_const) consts
         |-> (fn cs => pair (SOME cs))