src/Tools/nbe.ML
changeset 39134 917b4b6ba3d2
parent 38931 5e84c11c4b8a
child 39288 f1ae2493d93f
     1.1 --- a/src/Tools/nbe.ML	Sun Sep 05 19:47:40 2010 +0200
     1.2 +++ b/src/Tools/nbe.ML	Sun Sep 05 21:41:24 2010 +0200
     1.3 @@ -552,10 +552,11 @@
     1.4        singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
     1.5          (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
     1.6        (Type_Infer.constrain ty' t);
     1.7 -    fun check_tvars t = if null (Term.add_tvars t []) then t else
     1.8 -      error ("Illegal schematic type variables in normalized term: "
     1.9 -        ^ setmp_CRITICAL show_types true (Syntax.string_of_term_global thy) t);
    1.10 -    val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term_global thy);
    1.11 +    val string_of_term =
    1.12 +      Syntax.string_of_term (Config.put show_types true (Syntax.init_pretty_global thy));
    1.13 +    fun check_tvars t =
    1.14 +      if null (Term.add_tvars t []) then t
    1.15 +      else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
    1.16    in
    1.17      compile_eval thy program (vs, t) deps
    1.18      |> traced (fn t => "Normalized:\n" ^ string_of_term t)