author | wenzelm |
Sun, 18 May 2008 17:03:26 +0200 | |
changeset 26960 | 1aa5cd390dfb |
parent 26959 | f8f2df3e4d83 |
child 26961 | 290e1571c829 |
--- a/src/Pure/Isar/proof_context.ML Sun May 18 17:03:24 2008 +0200 +++ b/src/Pure/Isar/proof_context.ML Sun May 18 17:03:26 2008 +0200 @@ -657,7 +657,7 @@ |> Sign.extern_term (Consts.extern_early consts) thy |> LocalSyntax.extern_term syntax |> Syntax.standard_unparse_term (Consts.extern consts) ctxt (LocalSyntax.syn_of syntax) - (Context.exists_name Context.CPureN thy) + (not (PureThy.old_appl_syntax thy)) end; in