# HG changeset patch
# User wenzelm
# Date 1152035389 -7200
# Node ID c8018518e112cd0f0c192a2593b2310d9fddd946
# Parent  fe69952f09f6f1ba2d0d84e4f3bdec69f668240b
Thm.varifyT;

diff -r fe69952f09f6 -r c8018518e112 src/HOL/Import/proof_kernel.ML
--- 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
diff -r fe69952f09f6 -r c8018518e112 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Tue Jul 04 19:49:47 2006 +0200
+++ b/src/HOL/Import/shuffler.ML	Tue Jul 04 19:49:49 2006 +0200
@@ -269,7 +269,7 @@
     let
 	val cU = ctyp_of sg U
 	val tfrees = add_term_tfrees (prop_of thm,[])
-	val (rens, thm') = varifyT'
+	val (rens, thm') = Thm.varifyT'
     (gen_rem (op = o apfst fst) (tfrees, name)) thm
 	val mid = 
 	    case rens of
@@ -596,7 +596,7 @@
 	fun process [] = NONE
 	  | process ((name,th)::thms) =
 	    let
-		val norm_th = varifyT (norm_thm thy (close_thm (Thm.transfer sg th)))
+		val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer sg th)))
 		val triv_th = trivial rhs
 		val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
 		val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of