src/Pure/logic.ML
changeset 20078 f4122d7494f3
parent 19879 6a346150611a
child 20548 8ef25fe585a8
     1.1 --- a/src/Pure/logic.ML	Tue Jul 11 12:17:02 2006 +0200
     1.2 +++ b/src/Pure/logic.ML	Tue Jul 11 12:17:03 2006 +0200
     1.3 @@ -232,7 +232,7 @@
     1.4  (* type arities *)
     1.5  
     1.6  fun mk_arities (t, Ss, S) =
     1.7 -  let val T = Type (t, ListPair.map TFree (Term.invent_names [] "'a" (length Ss), Ss))
     1.8 +  let val T = Type (t, ListPair.map TFree (Name.invent_list [] "'a" (length Ss), Ss))
     1.9    in map (fn c => mk_inclass (T, c)) S end;
    1.10  
    1.11  fun dest_arity tm =
    1.12 @@ -486,7 +486,7 @@
    1.13      let val params = strip_params A;
    1.14          val vars = if !auto_rename
    1.15                     then rename_vars (!rename_prefix, params)
    1.16 -                   else ListPair.zip (variantlist(map #1 params,[]),
    1.17 +                   else ListPair.zip (Name.variant_list [] (map #1 params),
    1.18                                        map #2 params)
    1.19      in  list_all (vars, remove_params (length vars) n A)
    1.20      end;