1.1 --- a/src/Tools/code/code_ml.ML	Thu May 14 15:09:47 2009 +0200
     1.2 +++ b/src/Tools/code/code_ml.ML	Thu May 14 15:09:48 2009 +0200
     1.3 @@ -996,7 +996,7 @@
     1.4      val (ml_code, target_names) = eval_code_of NONE thy naming program (consts' @ tycos');
     1.5      val (consts'', tycos'') = chop (length consts') target_names;
     1.6      val consts_map = map2 (fn const => fn NONE =>
     1.7 -        error ("Constant " ^ (quote o Code_Unit.string_of_const thy) const
     1.8 +        error ("Constant " ^ (quote o Code.string_of_const thy) const
     1.9            ^ "\nhas a user-defined serialization")
    1.10        | SOME const'' => (const, const'')) consts consts''
    1.11      val tycos_map = map2 (fn tyco => fn NONE =>
    1.12 @@ -1050,7 +1050,7 @@
    1.13  
    1.14  fun ml_code_antiq raw_const {struct_name, background} =
    1.15    let
    1.16 -    val const = Code_Unit.check_const (ProofContext.theory_of background) raw_const;
    1.17 +    val const = Code.check_const (ProofContext.theory_of background) raw_const;
    1.18      val is_first = is_first_occ background;
    1.19      val background' = register_const const background;
    1.20    in (print_code struct_name is_first (print_const const), background') end;
    1.21 @@ -1059,7 +1059,7 @@
    1.22    let
    1.23      val thy = ProofContext.theory_of background;
    1.24      val tyco = Sign.intern_type thy raw_tyco;
    1.25 -    val constrs = map (Code_Unit.check_const thy) raw_constrs;
    1.26 +    val constrs = map (Code.check_const thy) raw_constrs;
    1.27      val constrs' = (map fst o snd o Code.get_datatype thy) tyco;
    1.28      val _ = if gen_eq_set (op =) (constrs, constrs') then ()
    1.29        else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors")