src/HOL/Import/proof_kernel.ML
changeset 24976 821628d16552
parent 24712 64ed05609568
child 26336 a0e2b706ce73
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Oct 11 18:58:34 2007 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Oct 11 19:10:17 2007 +0200
     1.3 @@ -2030,7 +2030,7 @@
     1.4  				 names'
     1.5  				 (thy1,th)
     1.6  	    val _ = ImportRecorder.add_specification names' th
     1.7 -	    val res' = Drule.unvarify res
     1.8 +	    val res' = Thm.unvarify res
     1.9  	    val hth = HOLThm(rens,res')
    1.10  	    val rew = rewrite_hol4_term (concl_of res') thy'
    1.11  	    val th  = equal_elim rew res'