*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] theory_of_thm @{thm xxx}*From*: Thomas Sewell <Thomas.Sewell at nicta.com.au>*Date*: Wed, 22 Aug 2012 15:31:21 +1000*In-reply-to*: <1345567640.6244.6.camel@lapbroy33>*References*: <1345567640.6244.6.camel@lapbroy33>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:11.0) Gecko/20120410 Thunderbird/11.0.1

In practice, this would create a problem if you tried, say: theory Scratch imports A B begin ML_val {* Thm.transitive @{thm A.eq1} @{thm B.eq2} *}

Yours, Thomas. On 22/08/12 02:47, Peter Lammich wrote:

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

**Follow-Ups**:**Re: [isabelle] theory_of_thm @{thm xxx}***From:*Peter Lammich

**Re: [isabelle] theory_of_thm @{thm xxx}***From:*Makarius

**References**:**[isabelle] theory_of_thm @{thm xxx}***From:*Peter Lammich

- Previous by Date: [isabelle] Reports like command/ctrl‑mouse‑hover in Output pan?
- Next by Date: Re: [isabelle] theory_of_thm @{thm xxx}
- Previous by Thread: [isabelle] theory_of_thm @{thm xxx}
- Next by Thread: Re: [isabelle] theory_of_thm @{thm xxx}
- Cl-isabelle-users August 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list