[isabelle] theory_of_thm @{thm xxx}

Hi all,

consider the following toy example:

theory Scratch
imports Pure

ML_val {*
  theory_of_thm @{thm meta_mp}

Output: val it = {Pure, Scratch:1}: theory

Why is Scratch contained in here? The theorem is defined in Pure, not in
Is there a way to reference to the theorem by name such that its theory
is the one it was defined in, and not the one the antiquotation occurs
In my real application (using HOL instead of Pure), I get odd
"non-trivial theory-merge" exceptions, because "theory_of_thm @{thm
xxx}" contains too much.

Regards and thanks in advance for any help,

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