src/Tools/nbe.ML

 fun nbe_abss 0 f = f `$` ml_list []
   | nbe_abss n f = name_abss `$$` [string_of_int n, f];
 
 end;
 
-open BasicCodeThingol;
+open Basic_Code_Thingol;
 
 (* code generation *)
 
 fun assemble_eqnss idx_of deps eqnss =
   let

 
     fun assemble_iterm constapp =
       let
         fun of_iterm t =
           let
-            val (t', ts) = CodeThingol.unfold_app t
+            val (t', ts) = Code_Thingol.unfold_app t
           in of_iapp t' (fold_rev (cons o of_iterm) ts []) end
         and of_iapp (IConst (c, (dss, _))) ts = constapp c dss ts
           | of_iapp (IVar v) ts = nbe_apps (nbe_bound v) ts
           | of_iapp ((v, _) `|-> t) ts =
               nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm t))) ts

         |> (fn univs => cs ~~ univs)
       end;
 
 (* preparing function equations *)
 
-fun eqns_of_stmt (_, CodeThingol.Fun (_, [])) =
+fun eqns_of_stmt (_, Code_Thingol.Fun (_, [])) =
       []
-  | eqns_of_stmt (const, CodeThingol.Fun ((vs, _), eqns)) =
+  | eqns_of_stmt (const, Code_Thingol.Fun ((vs, _), eqns)) =
       [(const, (vs, map fst eqns))]
-  | eqns_of_stmt (_, CodeThingol.Datatypecons _) =
+  | eqns_of_stmt (_, Code_Thingol.Datatypecons _) =
       []
-  | eqns_of_stmt (_, CodeThingol.Datatype _) =
+  | eqns_of_stmt (_, Code_Thingol.Datatype _) =
       []
-  | eqns_of_stmt (class, CodeThingol.Class (v, (superclasses, classops))) =
+  | eqns_of_stmt (class, Code_Thingol.Class (v, (superclasses, classops))) =
       let
         val names = map snd superclasses @ map fst classops;
         val params = Name.invent_list [] "d" (length names);
         fun mk (k, name) =
           (name, ([(v, [])],
             [([IConst (class, ([], [])) `$$ map IVar params], IVar (nth params k))]));
       in map_index mk names end
-  | eqns_of_stmt (_, CodeThingol.Classrel _) =
+  | eqns_of_stmt (_, Code_Thingol.Classrel _) =
       []
-  | eqns_of_stmt (_, CodeThingol.Classparam _) =
+  | eqns_of_stmt (_, Code_Thingol.Classparam _) =
       []
-  | eqns_of_stmt (inst, CodeThingol.Classinst ((class, (_, arities)), (superinsts, instops))) =
+  | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arities)), (superinsts, instops))) =
       [(inst, (arities, [([], IConst (class, ([], [])) `$$
         map (fn (_, (_, (inst, dicts))) => IConst (inst, (dicts, []))) superinsts
         @ map (IConst o snd o fst) instops)]))];
 
 fun compile_stmts stmts_deps =

 
 (* term evaluation *)
 
 fun eval_term gr deps ((vs, ty), t) =
   let 
-    val frees = CodeThingol.fold_unbound_varnames (insert (op =)) t []
+    val frees = Code_Thingol.fold_unbound_varnames (insert (op =)) t []
     val frees' = map (fn v => Free (v, [])) frees;
     val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
   in
     ("", (vs, [(map IVar frees, t)]))
     |> singleton (compile_eqnss gr deps)

       | take_until f (x::xs) = if f x then [] else x :: take_until f xs;
     fun is_dict (Const (idx, _)) =
           let
             val c = the (Inttab.lookup idx_tab idx);
           in
-            (is_some o CodeName.class_rev thy) c
-            orelse (is_some o CodeName.classrel_rev thy) c
-            orelse (is_some o CodeName.instance_rev thy) c
+            (is_some o Code_Name.class_rev thy) c
+            orelse (is_some o Code_Name.classrel_rev thy) c
+            orelse (is_some o Code_Name.instance_rev thy) c
           end
       | is_dict (DFree _) = true
       | is_dict _ = false;
     fun of_apps bounds (t, ts) =
       fold_map (of_univ bounds) ts
       #>> (fn ts' => list_comb (t, rev ts'))
     and of_univ bounds (Const (idx, ts)) typidx =
           let
             val ts' = take_until is_dict ts;
-            val c = (the o CodeName.const_rev thy o the o Inttab.lookup idx_tab) idx;
+            val c = (the o Code_Name.const_rev thy o the o Inttab.lookup idx_tab) idx;
             val (_, T) = Code.default_typ thy c;
             val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, [])) T;
             val typidx' = typidx + maxidx_of_typ T' + 1;
           in of_apps bounds (Term.Const (c, T'), ts') typidx' end
       | of_univ bounds (Free (name, ts)) typidx =

   type T = (Univ option * int) Graph.T * (int * string Inttab.table);
   val empty = (Graph.empty, (0, Inttab.empty));
   fun purge thy cs (gr, (maxidx, idx_tab)) =
     let
       val cs_exisiting =
-        map_filter (CodeName.const_rev thy) (Graph.keys gr);
+        map_filter (Code_Name.const_rev thy) (Graph.keys gr);
       val dels = (Graph.all_preds gr
-          o map (CodeName.const thy)
+          o map (Code_Name.const thy)
           o filter (member (op =) cs_exisiting)
         ) cs;
     in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end;
 );
 

 
 fun eval thy t program vs_ty_t deps =
   let
     fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
       | t => t);
-    val subst_triv_consts = subst_const (CodeUnit.resubst_alias thy);
+    val subst_triv_consts = subst_const (Code_Unit.resubst_alias thy);
     val ty = type_of t;
     val type_free = AList.lookup (op =)
       (map (fn (s, T) => (s, Term.Free (s, T))) (Term.add_frees t []));
     val type_frees = Term.map_aterms
       (fn (t as Term.Free (s, _)) => the_default t (type_free s) | t => t);

     |> tracing (fn t => "---\n")
   end;
 
 (* evaluation oracle *)
 
-exception Norm of term * CodeThingol.program
-  * (CodeThingol.typscheme * CodeThingol.iterm) * string list;
+exception Norm of term * Code_Thingol.program
+  * (Code_Thingol.typscheme * Code_Thingol.iterm) * string list;
 
 fun norm_oracle (thy, Norm (t, program, vs_ty_t, deps)) =
   Logic.mk_equals (t, eval thy t program vs_ty_t deps);
 
 fun norm_invoke thy t program vs_ty_t deps =

   (*FIXME get rid of hardwired theory name*)
 
 fun add_triv_classes thy =
   let
     val inters = curry (Sorts.inter_sort (Sign.classes_of thy))
-      (CodeUnit.triv_classes thy);
+      (Code_Unit.triv_classes thy);
     fun map_sorts f = (map_types o map_atyps)
       (fn TVar (v, sort) => TVar (v, f sort)
         | TFree (v, sort) => TFree (v, f sort));
   in map_sorts inters end;
 
 fun norm_conv ct =
   let
     val thy = Thm.theory_of_cterm ct;
     fun evaluator' t program vs_ty_t deps = norm_invoke thy t program vs_ty_t deps;
     fun evaluator t = (add_triv_classes thy t, evaluator' t);
-  in CodeThingol.eval_conv thy evaluator ct end;
+  in Code_Thingol.eval_conv thy evaluator ct end;
 
 fun norm_term thy t =
   let
     fun evaluator' t program vs_ty_t deps = eval thy t program vs_ty_t deps;
     fun evaluator t = (add_triv_classes thy t, evaluator' t);
-  in (Code.postprocess_term thy o CodeThingol.eval_term thy evaluator) t end;
+  in (Code.postprocess_term thy o Code_Thingol.eval_term thy evaluator) t end;
 
 (* evaluation command *)
 
 fun norm_print_term ctxt modes t =
   let