src/HOL/Import/shuffler.ML
changeset 19998 c8018518e112
parent 18728 6790126ab5f6
child 20071 8f3e1ddb50e6
     1.1 --- a/src/HOL/Import/shuffler.ML	Tue Jul 04 19:49:47 2006 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Tue Jul 04 19:49:49 2006 +0200
     1.3 @@ -269,7 +269,7 @@
     1.4      let
     1.5  	val cU = ctyp_of sg U
     1.6  	val tfrees = add_term_tfrees (prop_of thm,[])
     1.7 -	val (rens, thm') = varifyT'
     1.8 +	val (rens, thm') = Thm.varifyT'
     1.9      (gen_rem (op = o apfst fst) (tfrees, name)) thm
    1.10  	val mid = 
    1.11  	    case rens of
    1.12 @@ -596,7 +596,7 @@
    1.13  	fun process [] = NONE
    1.14  	  | process ((name,th)::thms) =
    1.15  	    let
    1.16 -		val norm_th = varifyT (norm_thm thy (close_thm (Thm.transfer sg th)))
    1.17 +		val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer sg th)))
    1.18  		val triv_th = trivial rhs
    1.19  		val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
    1.20  		val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of