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