# HG changeset patch # User wenzelm # Date 1211115888 -7200 # Node ID df36f4c52ee8daa090920e7388ec15032cc5ef11 # Parent 030e4a818b39e1a6a1c83a0db2661e560de4a4bf command 'normal_form': proper context via Variable.auto_fixes; diff -r 030e4a818b39 -r df36f4c52ee8 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Sun May 18 15:04:46 2008 +0200 +++ b/src/Tools/nbe.ML Sun May 18 15:04:48 2008 +0200 @@ -386,14 +386,14 @@ val type_frees = Term.map_aterms (fn (t as Term.Free (s, _)) => the_default t (type_free s) | t => t); fun type_infer t = [(t, ty)] - |> TypeInfer.infer_types (Sign.pp thy) (Sign.tsig_of thy) I + |> TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0 NONE |> fst |> the_single |> fst; fun check_tvars t = if null (Term.term_tvars t) then t else error ("Illegal schematic type variables in normalized term: " - ^ setmp show_types true (Sign.string_of_term thy) t); - val string_of_term = setmp show_types true (Sign.string_of_term thy); + ^ setmp show_types true (Syntax.string_of_term_global thy) t); + val string_of_term = setmp show_types true (Syntax.string_of_term_global thy); in compile_eval thy code vs_ty_t deps |> tracing (fn t => "Normalized:\n" ^ string_of_term t) @@ -447,9 +447,10 @@ val thy = ProofContext.theory_of ctxt; val t' = norm_term thy t; val ty' = Term.type_of t'; + val ctxt' = Variable.auto_fixes t ctxt; val p = PrintMode.with_modes modes (fn () => - Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t'), Pretty.fbrk, - Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt ty')]) (); + Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk, + Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) (); in Pretty.writeln p end;