src/Pure/Proof/extraction.ML
changeset 60826 695cf1fab6cc
parent 59787 6e2a20486897
child 61039 80f40d89dab6
     1.1 --- a/src/Pure/Proof/extraction.ML	Tue Jul 28 21:47:03 2015 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Tue Jul 28 23:14:40 2015 +0200
     1.3 @@ -769,9 +769,9 @@
     1.4  
     1.5        | extr d vs ts Ts hs _ defs = error "extr: bad proof";
     1.6  
     1.7 -    fun prep_thm vs thm =
     1.8 +    fun prep_thm vs raw_thm =
     1.9        let
    1.10 -        val thy = Thm.theory_of_thm thm;
    1.11 +        val thm = Thm.transfer thy raw_thm;
    1.12          val prop = Thm.prop_of thm;
    1.13          val prf = Thm.proof_of thm;
    1.14          val name = Thm.derivation_name thm;