# [isabelle] theory_of_thm @{thm xxx}

Hi all,
consider the following toy example:
theory Scratch
imports Pure
begin
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
Scratch.
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?
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,
Peter

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