--- a/src/HOL/Tools/inductive_package.ML Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/inductive_package.ML Tue Jul 11 12:16:54 2006 +0200
@@ -324,7 +324,7 @@
fun mk_elims cs cTs params intr_ts intr_names =
let
val used = foldr add_term_names [] intr_ts;
- val [aname, pname] = variantlist (["a", "P"], used);
+ val [aname, pname] = Name.variant_list used ["a", "P"];
val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
fun dest_intr r =
@@ -359,8 +359,8 @@
(* predicates for induction rule *)
- val preds = map Free (variantlist (if length cs < 2 then ["P"] else
- map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
+ val preds = map Free (Name.variant_list used (if length cs < 2 then ["P"] else
+ map (fn i => "P" ^ string_of_int i) (1 upto length cs)) ~~
map (fn T => T --> HOLogic.boolT) cTs);
(* transform an introduction rule into a premise for induction rule *)
@@ -697,7 +697,7 @@
val fp_name = if coind then gfp_name else lfp_name;
val used = foldr add_term_names [] intr_ts;
- val [sname, xname] = variantlist (["S", "x"], used);
+ val [sname, xname] = Name.variant_list used ["S", "x"];
(* transform an introduction rule into a conjunction *)
(* [| t : ... S_i ... ; ... |] ==> u : S_j *)