1.1 --- a/src/Tools/code/code_thingol.ML	Thu May 14 15:09:47 2009 +0200
     1.2 +++ b/src/Tools/code/code_thingol.ML	Thu May 14 15:09:48 2009 +0200
     1.3 @@ -498,7 +498,7 @@
     1.4        let
     1.5          val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty
     1.6            then raw_thms
     1.7 -          else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms;
     1.8 +          else (map o apfst) (Code.expand_eta thy 1) raw_thms;
     1.9        in
    1.10          fold_map (translate_tyvar_sort thy algbr funcgr) vs
    1.11          ##>> translate_typ thy algbr funcgr ty
    1.12 @@ -634,7 +634,7 @@
    1.13          Term.strip_abs_eta 1 (the_single ts_clause)
    1.14        in [(true, (Free v_ty, body))] end
    1.15        else map (uncurry mk_clause)
    1.16 -        (AList.make (Code_Unit.no_args thy) case_pats ~~ ts_clause);
    1.17 +        (AList.make (Code.no_args thy) case_pats ~~ ts_clause);
    1.18      fun retermify ty (_, (IVar x, body)) =
    1.19            (x, ty) `|-> body
    1.20        | retermify _ (_, (pat, body)) =
    1.21 @@ -812,7 +812,7 @@
    1.22      fun read_const_expr "*" = ([], consts_of NONE)
    1.23        | read_const_expr s = if String.isSuffix ".*" s
    1.24            then ([], consts_of (SOME (unsuffix ".*" s)))
    1.25 -          else ([Code_Unit.read_const thy s], []);
    1.26 +          else ([Code.read_const thy s], []);
    1.27    in pairself flat o split_list o map read_const_expr end;
    1.28  
    1.29  fun code_depgr thy consts =
    1.30 @@ -839,7 +839,7 @@
    1.31        |> map (the o Symtab.lookup mapping)
    1.32        |> distinct (op =);
    1.33      val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
    1.34 -    fun namify consts = map (Code_Unit.string_of_const thy) consts
    1.35 +    fun namify consts = map (Code.string_of_const thy) consts
    1.36        |> commas;
    1.37      val prgr = map (fn (consts, constss) =>
    1.38        { name = namify consts, ID = namify consts, dir = "", unfold = true,