src/Pure/drule.ML
changeset 20077 4fc9a4fef219
parent 19999 9592df0c3176
child 20227 435601e8e53d
     1.1 --- a/src/Pure/drule.ML	Tue Jul 11 12:17:01 2006 +0200
     1.2 +++ b/src/Pure/drule.ML	Tue Jul 11 12:17:02 2006 +0200
     1.3 @@ -370,10 +370,8 @@
     1.4  val forall_elim_vars = PureThy.forall_elim_vars;
     1.5  
     1.6  fun outer_params t =
     1.7 -  let
     1.8 -    val vs = Term.strip_all_vars t;
     1.9 -    val clean_name = perhaps (try Term.dest_skolem) #> perhaps (try Term.dest_internal);
    1.10 -  in Term.variantlist (map (clean_name o #1) vs, []) ~~ map #2 vs end;
    1.11 +  let val vs = Term.strip_all_vars t
    1.12 +  in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;
    1.13  
    1.14  (*generalize outermost parameters*)
    1.15  fun gen_all th =
    1.16 @@ -500,7 +498,7 @@
    1.17         [] => (fth, fn x => x)
    1.18       | vars =>
    1.19           let fun newName (Var(ix,_), (pairs,used)) =
    1.20 -                   let val v = variant used (string_of_indexname ix)
    1.21 +                   let val v = Name.variant used (string_of_indexname ix)
    1.22                     in  ((ix,v)::pairs, v::used)  end;
    1.23               val (alist, _) = foldr newName ([], Library.foldr add_term_names
    1.24                 (prop :: Thm.terms_of_tpairs tpairs, [])) vars