Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Import/proof_kernel.ML
changeset 24976 821628d16552
parent 24712 64ed05609568
child 26336 a0e2b706ce73 
--- a/src/HOL/Import/proof_kernel.ML	Thu Oct 11 18:58:34 2007 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu Oct 11 19:10:17 2007 +0200
@@ -2030,7 +2030,7 @@
 				 names'
 				 (thy1,th)
 	    val _ = ImportRecorder.add_specification names' th
-	    val res' = Drule.unvarify res
+	    val res' = Thm.unvarify res
 	    val hth = HOLThm(rens,res')
 	    val rew = rewrite_hol4_term (concl_of res') thy'
 	    val th  = equal_elim rew res'
isabelle