[isabelle] print_statement does not quote variables with reserved names



Dear list,

I occasionally (e.g., when I refactor my theories) use print_statement some_thm to get long statement of a theorem printed such that I can copy-paste the fixes and assumes part into a "context fixes ... assumes ... begin" block. Now, I noticed that when a variable has the name is reserved in the current outer syntax (for example, a variable called oracle), then there are no quotes around the fixed variable.

Here's an example:

  lemma foo: "oracle = 0 ==> 0 = oracle" by simp
  print_statement foo
  (* output:
  theorem foo:
    fixes oracle :: "'a"
      and x :: "'a"
    assumes "oracle = x"
    shows "x = oracle"
  *)

Could print_statement be changed such that the output encloses the variable "oracle" in quotes? I.e.:

  theorem foo:
    fixes "oracle" :: "'a"
      and x :: "'a"
    assumes "oracle = x"
    shows "x = oracle"


Thanks,
Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.