replaced Term.variant(list) by Name.variant(_list);
authorwenzelm
Tue, 11 Jul 2006 12:17:03 +0200
changeset 20078 f4122d7494f3
parent 20077 4fc9a4fef219
child 20079 ec5c8584487c
replaced Term.variant(list) by Name.variant(_list); Name.invent_list;
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;