# HG changeset patch
# User wenzelm
# Date 1152613023 -7200
# Node ID f4122d7494f36009b1a1b553dc3b759d2e11ea35
# Parent  4fc9a4fef2192e381d1b96dfb095bb4f9715c5f0
replaced Term.variant(list) by Name.variant(_list);
Name.invent_list;

diff -r 4fc9a4fef219 -r f4122d7494f3 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Tue Jul 11 12:17:02 2006 +0200
+++ b/src/Pure/logic.ML	Tue Jul 11 12:17:03 2006 +0200
@@ -232,7 +232,7 @@
 (* type arities *)
 
 fun mk_arities (t, Ss, S) =
-  let val T = Type (t, ListPair.map TFree (Term.invent_names [] "'a" (length Ss), Ss))
+  let val T = Type (t, ListPair.map TFree (Name.invent_list [] "'a" (length Ss), Ss))
   in map (fn c => mk_inclass (T, c)) S end;
 
 fun dest_arity tm =
@@ -486,7 +486,7 @@
     let val params = strip_params A;
         val vars = if !auto_rename
                    then rename_vars (!rename_prefix, params)
-                   else ListPair.zip (variantlist(map #1 params,[]),
+                   else ListPair.zip (Name.variant_list [] (map #1 params),
                                       map #2 params)
     in  list_all (vars, remove_params (length vars) n A)
     end;