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