1.1 --- a/src/Tools/nbe.ML	Thu May 27 15:28:23 2010 +0200
     1.2 +++ b/src/Tools/nbe.ML	Thu May 27 17:41:27 2010 +0200
     1.3 @@ -506,7 +506,7 @@
     1.4              val ts' = take_until is_dict ts;
     1.5              val c = const_of_idx idx;
     1.6              val T = map_type_tvar (fn ((v, i), _) =>
     1.7 -              TypeInfer.param typidx (v ^ string_of_int i, []))
     1.8 +              Type_Infer.param typidx (v ^ string_of_int i, []))
     1.9                  (Sign.the_const_type thy c);
    1.10              val typidx' = typidx + 1;
    1.11            in of_apps bounds (Term.Const (c, T), ts') typidx' end
    1.12 @@ -548,9 +548,9 @@
    1.13    let
    1.14      val ty' = typ_of_itype program vs0 ty;
    1.15      fun type_infer t =
    1.16 -      singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
    1.17 +      singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
    1.18          (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
    1.19 -      (TypeInfer.constrain ty' t);
    1.20 +      (Type_Infer.constrain ty' t);
    1.21      fun check_tvars t = if null (Term.add_tvars t []) then t else
    1.22        error ("Illegal schematic type variables in normalized term: "
    1.23          ^ setmp_CRITICAL show_types true (Syntax.string_of_term_global thy) t);