[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.