src/HOL/Import/shuffler.ML
changeset 20951 868120282837
parent 20897 3f8d2834b2c4
child 21078 101aefd61aac
     1.1 --- a/src/HOL/Import/shuffler.ML	Tue Oct 10 13:59:12 2006 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Tue Oct 10 13:59:13 2006 +0200
     1.3 @@ -270,7 +270,7 @@
     1.4  	val cU = ctyp_of sg U
     1.5  	val tfrees = add_term_tfrees (prop_of thm,[])
     1.6  	val (rens, thm') = Thm.varifyT'
     1.7 -    (gen_rem (op = o apfst fst) (tfrees, name)) thm
     1.8 +    (remove (op = o apsnd fst) name tfrees) thm
     1.9  	val mid = 
    1.10  	    case rens of
    1.11  		[] => thm'