| changeset 19998 | c8018518e112 |
| parent 19873 | 588329441a78 |
| child 20286 | 4cf8e86a2d29 |
--- a/src/HOL/Import/proof_kernel.ML Tue Jul 04 19:49:47 2006 +0200 +++ b/src/HOL/Import/proof_kernel.ML Tue Jul 04 19:49:49 2006 +0200 @@ -1422,7 +1422,7 @@ val _ = message "INST_TYPE:" val _ = if_debug pth hth val tys_before = add_term_tfrees (prop_of th,[]) - val th1 = varifyT th + val th1 = Thm.varifyT th val tys_after = add_term_tvars (prop_of th1,[]) val tyinst = map (fn (bef, iS) => (case try (Lib.assoc (TFree bef)) lambda of