src/HOL/Import/shuffler.ML
changeset 15794 5de27a5fc5ed
parent 15661 9ef583b08647
child 16428 d2203a276b07
     1.1 --- a/src/HOL/Import/shuffler.ML	Thu Apr 21 18:56:03 2005 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Thu Apr 21 18:57:18 2005 +0200
     1.3 @@ -268,12 +268,14 @@
     1.4    | inst_tfrees sg ((name,U)::rest) thm = 
     1.5      let
     1.6  	val cU = ctyp_of sg U
     1.7 -	val tfree_names = add_term_tfree_names (prop_of thm,[])
     1.8 -	val (thm',rens) = varifyT' (tfree_names \ name) thm
     1.9 +	val tfrees = add_term_tfrees (prop_of thm,[])
    1.10 +	val (thm',rens) = varifyT'
    1.11 +    (gen_rem (op = o apfst fst) (tfrees, name)) thm
    1.12  	val mid = 
    1.13  	    case rens of
    1.14  		[] => thm'
    1.15 -	      | [(_,idx)] => instantiate ([(idx,cU)],[]) thm'
    1.16 +	      | [((_, S), idx)] => instantiate
    1.17 +            ([(ctyp_of sg (TVar (idx, S)), cU)], []) thm'
    1.18  	      | _ => error "Shuffler.inst_tfrees internal error"
    1.19      in
    1.20  	inst_tfrees sg rest mid