--- 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
--- 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