# HG changeset patch
# User wenzelm
# Date 1211123006 -7200
# Node ID 1aa5cd390dfbb92bf07b4990111d5a80f9062632
# Parent  f8f2df3e4d83d743ed03b8f936afac594d5f270c
unparse_term: check PureThy.old_appl_syntax instead of CPure;

diff -r f8f2df3e4d83 -r 1aa5cd390dfb src/Pure/Isar/proof_context.ML
--- 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