1.1 --- a/src/Tools/nbe.ML	Thu May 14 15:09:47 2009 +0200
     1.2 +++ b/src/Tools/nbe.ML	Thu May 14 15:09:48 2009 +0200
     1.3 @@ -436,7 +436,7 @@
     1.4    let
     1.5      fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
     1.6        | t => t);
     1.7 -    val resubst_triv_consts = subst_const (Code_Unit.resubst_alias thy);
     1.8 +    val resubst_triv_consts = subst_const (Code.resubst_alias thy);
     1.9      val ty' = typ_of_itype program vs0 ty;
    1.10      fun type_infer t =
    1.11        singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
    1.12 @@ -459,7 +459,7 @@
    1.13  (* evaluation oracle *)
    1.14  
    1.15  fun add_triv_classes thy = curry (Sorts.inter_sort (Sign.classes_of thy))
    1.16 -  (Code_Unit.triv_classes thy);
    1.17 +  (Code.triv_classes thy);
    1.18  
    1.19  fun mk_equals thy lhs raw_rhs =
    1.20    let