unparse_term: check PureThy.old_appl_syntax instead of CPure;
authorwenzelm
Sun, 18 May 2008 17:03:26 +0200
changeset 26960 1aa5cd390dfb
parent 26959 f8f2df3e4d83
child 26961 290e1571c829
unparse_term: check PureThy.old_appl_syntax instead of CPure;
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