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 19873 588329441a78
parent 19686 83611262823e
child 19998 c8018518e112 
--- a/src/HOL/Import/proof_kernel.ML	Tue Jun 13 15:42:52 2006 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Tue Jun 13 23:41:31 2006 +0200
@@ -2029,7 +2029,7 @@
 				 names'
 				 (thy1,th)
 	    val _ = ImportRecorder.add_specification names' th
-	    val res' = Drule.freeze_all res
+	    val res' = Drule.unvarify res
 	    val hth = HOLThm(rens,res')
 	    val rew = rewrite_hol4_term (concl_of res') thy'
 	    val th  = equal_elim rew res'
isabelle