unparse_term: check PureThy.old_appl_syntax instead of CPure;
authorwenzelm
Sun May 18 17:03:26 2008 +0200 (2008-05-18 ago)
changeset 269601aa5cd390dfb
parent 26959 f8f2df3e4d83
child 26961 290e1571c829
unparse_term: check PureThy.old_appl_syntax instead of CPure;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sun May 18 17:03:24 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sun May 18 17:03:26 2008 +0200
     1.3 @@ -657,7 +657,7 @@
     1.4      |> Sign.extern_term (Consts.extern_early consts) thy
     1.5      |> LocalSyntax.extern_term syntax
     1.6      |> Syntax.standard_unparse_term (Consts.extern consts) ctxt (LocalSyntax.syn_of syntax)
     1.7 -        (Context.exists_name Context.CPureN thy)
     1.8 +        (not (PureThy.old_appl_syntax thy))
     1.9    end;
    1.10  
    1.11  in