src/HOL/Import/shuffler.ML
changeset 20071 8f3e1ddb50e6
parent 19998 c8018518e112
child 20224 9c40a144ee0e
     1.1 --- a/src/HOL/Import/shuffler.ML	Tue Jul 11 12:16:52 2006 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Tue Jul 11 12:16:54 2006 +0200
     1.3 @@ -253,7 +253,7 @@
     1.4  	val (type_inst,_) =
     1.5  	    Library.foldl (fn ((inst,used),(w as (v,_),S)) =>
     1.6  		      let
     1.7 -			  val v' = variant used v
     1.8 +			  val v' = Name.variant used v
     1.9  		      in
    1.10  			  ((w,TFree(v',S))::inst,v'::used)
    1.11  		      end)
    1.12 @@ -322,7 +322,7 @@
    1.13  	      then
    1.14  		  let
    1.15  		      val cert = cterm_of sg
    1.16 -		      val v = Free(variant (add_term_free_names(t,[])) "v",xT)
    1.17 +		      val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT)
    1.18  		      val cv = cert v
    1.19  		      val ct = cert t
    1.20  		      val th = (assume ct)
    1.21 @@ -385,7 +385,7 @@
    1.22  		      Type("fun",[aT,bT]) =>
    1.23  		      let
    1.24  			  val cert = cterm_of sg
    1.25 -			  val vname = variant (add_term_free_names(t,[])) "v"
    1.26 +			  val vname = Name.variant (add_term_free_names(t,[])) "v"
    1.27  			  val v = Free(vname,aT)
    1.28  			  val cv = cert v
    1.29  			  val ct = cert t