[isabelle-dev] print_theorems uses a wrong context?

[Ondřej Kunčar]

Dear Isabelle-Dev,
this refers to fbf4d50dec91.

Recently I started using interpretation in anonymous contexts to 
introduce syntax locally. But now I noticed that print_theorems behaves 
differently than I expected.

Consider this example:

context begin
interpretation lifting_syntax .

term "op ===>" -- {* we have the symbol ===> now *}

lemma x: "R ===> R = R ===> R" ..

thm x -- {* everything is OK *}

print_theorems -- {* but print_theorems still outputs fun_rel rather 
than ===> *}

end

Best,
Ondrej