# HG changeset patch
# User wenzelm
# Date 1152613014 -7200
# Node ID 8f3e1ddb50e62f6a184248a3968c7e6baf318330
# Parent  3f31fb81b83ae8e39786dea3eef7d6f570850ccb
replaced Term.variant(list) by Name.variant(_list);

diff -r 3f31fb81b83a -r 8f3e1ddb50e6 TFL/rules.ML
--- a/TFL/rules.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/TFL/rules.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -513,8 +513,8 @@
             let val eq = Logic.strip_imp_concl body
                 val (f,args) = S.strip_comb (get_lhs eq)
                 val (vstrl,_) = S.strip_abs f
-                val names  = variantlist (map (#1 o dest_Free) vstrl,
-                                          add_term_names(body, []))
+                val names  =
+                  Name.variant_list (add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
             in get (rst, n+1, (names,n)::L) end
             handle TERM _ => get (rst, n+1, L)
               | U.ERR _ => get (rst, n+1, L);
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 TFL/usyntax.ML
--- a/TFL/usyntax.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/TFL/usyntax.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -240,7 +240,7 @@
 
 fun dest_abs used (a as Abs(s, ty, M)) =
      let
-       val s' = variant used s;
+       val s' = Name.variant used s;
        val v = Free(s', ty);
      in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
      end
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Import/hol4rews.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -735,7 +735,7 @@
 		then F defname                 (* name_def *)
 		else if not (pdefname mem used)
 		then F pdefname                (* name_primdef *)
-		else F (variant used pdefname) (* last resort *)
+		else F (Name.variant used pdefname) (* last resort *)
 	    end
     end
 
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Import/shuffler.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -253,7 +253,7 @@
 	val (type_inst,_) =
 	    Library.foldl (fn ((inst,used),(w as (v,_),S)) =>
 		      let
-			  val v' = variant used v
+			  val v' = Name.variant used v
 		      in
 			  ((w,TFree(v',S))::inst,v'::used)
 		      end)
@@ -322,7 +322,7 @@
 	      then
 		  let
 		      val cert = cterm_of sg
-		      val v = Free(variant (add_term_free_names(t,[])) "v",xT)
+		      val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT)
 		      val cv = cert v
 		      val ct = cert t
 		      val th = (assume ct)
@@ -385,7 +385,7 @@
 		      Type("fun",[aT,bT]) =>
 		      let
 			  val cert = cterm_of sg
-			  val vname = variant (add_term_free_names(t,[])) "v"
+			  val vname = Name.variant (add_term_free_names(t,[])) "v"
 			  val v = Free(vname,aT)
 			  val cv = cert v
 			  val ct = cert t
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Tue Jul 11 12:16:54 2006 +0200
@@ -153,7 +153,7 @@
 fun remove_suc thy thms =
   let
     val Suc_if_eq' = Thm.transfer thy Suc_if_eq;
-    val vname = variant (map fst
+    val vname = Name.variant (map fst
       (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
     val cv = cterm_of Main.thy (Var ((vname, 0), HOLogic.natT));
     fun lhs_of th = snd (Thm.dest_comb
@@ -206,7 +206,7 @@
 fun remove_suc_clause thy thms =
   let
     val Suc_clause' = Thm.transfer thy Suc_clause;
-    val vname = variant (map fst
+    val vname = Name.variant (map fst
       (fold (add_term_varnames o Thm.full_prop_of) thms [])) "x";
     fun find_var (t as Const ("Suc", _) $ (v as Var _)) = SOME (t, v)
       | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -252,7 +252,7 @@
   let val used = add_term_names (t, [])
           and vars = term_vars t;
       fun newName (Var(ix,_), (pairs,used)) = 
-          let val v = variant used (string_of_indexname ix)
+          let val v = Name.variant used (string_of_indexname ix)
           in  ((ix,v)::pairs, v::used)  end;
       val (alist, _) = foldr newName ([], used) vars;
       fun mk_inst (Var(v,T)) = (Var(v,T),
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -553,7 +553,7 @@
               QUIET_BREADTH_FIRST (has_fewer_prems 1)
               (resolve_tac rep_intrs 1))) thy |> (fn (r, thy) =>
         let
-          val permT = mk_permT (TFree (variant tvs "'a", HOLogic.typeS));
+          val permT = mk_permT (TFree (Name.variant tvs "'a", HOLogic.typeS));
           val pi = Free ("pi", permT);
           val tvs' = map (fn s => TFree (s, the (AList.lookup op = sorts' s))) tvs;
           val T = Type (Sign.intern_type thy name, tvs');
@@ -1096,11 +1096,11 @@
         val recs = List.filter is_rec_type cargs;
         val Ts = map (typ_of_dtyp descr'' sorts') cargs;
         val recTs' = map (typ_of_dtyp descr'' sorts') recs;
-        val tnames = variantlist (DatatypeProp.make_tnames Ts, pnames);
+        val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
         val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
         val frees = tnames ~~ Ts;
         val frees' = partition_cargs idxs frees;
-        val z = (variant tnames "z", fsT);
+        val z = (Name.variant tnames "z", fsT);
 
         fun mk_prem ((dt, s), T) =
           let
@@ -1126,7 +1126,7 @@
         Const ("Nominal.fresh", T --> fsT --> HOLogic.boolT) $ t $ u) i T)
           (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs));
     val tnames = DatatypeProp.make_tnames recTs;
-    val zs = variantlist (replicate (length descr'') "z", tnames);
+    val zs = Name.variant_list tnames (replicate (length descr'') "z");
     val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
       (map (fn ((((i, _), T), tname), z) =>
         make_pred fsT i T $ Free (z, fsT) $ Free (tname, T))
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -280,7 +280,7 @@
     val recTs = get_rec_types descr' sorts;
     val used = foldr add_typ_tfree_names [] recTs;
     val newTs = Library.take (length (hd descr), recTs);
-    val T' = TFree (variant used "'t", HOLogic.typeS);
+    val T' = TFree (Name.variant used "'t", HOLogic.typeS);
 
     fun mk_dummyT dt = binder_types (typ_of_dtyp descr' sorts dt) ---> T';
 
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -219,7 +219,7 @@
           | pcase gr ((cname, cargs)::cs) (t::ts) (U::Us) =
               let
                 val j = length cargs;
-                val xs = variantlist (replicate j "x", names);
+                val xs = Name.variant_list names (replicate j "x");
                 val Us' = Library.take (j, fst (strip_type U));
                 val frees = map Free (xs ~~ Us');
                 val (gr0, cp) = invoke_codegen thy defs dep module false
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -609,7 +609,7 @@
     val size_names = DatatypeProp.indexify_names
       (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs)));
 
-    val freeT = TFree (variant used "'t", HOLogic.typeS);
+    val freeT = TFree (Name.variant used "'t", HOLogic.typeS);
     val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
         let val Ts = map (typ_of_dtyp descr' sorts) cargs
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -108,7 +108,7 @@
         val recs = List.filter is_rec_type cargs;
         val Ts = map (typ_of_dtyp descr' sorts) cargs;
         val recTs' = map (typ_of_dtyp descr' sorts) recs;
-        val tnames = variantlist (make_tnames Ts, pnames);
+        val tnames = Name.variant_list pnames (make_tnames Ts);
         val rec_tnames = map fst (List.filter (is_rec_type o snd) (tnames ~~ cargs));
         val frees = tnames ~~ Ts;
         val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
@@ -136,7 +136,7 @@
     fun make_casedist_prem T (cname, cargs) =
       let
         val Ts = map (typ_of_dtyp descr' sorts) cargs;
-        val frees = variantlist (make_tnames Ts, ["P", "y"]) ~~ Ts;
+        val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;
         val free_ts = map Free frees
       in list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
         (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
@@ -158,7 +158,7 @@
   let
     val descr' = List.concat descr;
 
-    val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
+    val rec_result_Ts = map TFree (Name.variant_list used (replicate (length descr') "'t") ~~
       replicate (length descr') HOLogic.typeS);
 
     val reccomb_fn_Ts = List.concat (map (fn (i, (_, _, constrs)) =>
@@ -234,7 +234,7 @@
     val recTs = get_rec_types descr' sorts;
     val used = foldr add_typ_tfree_names [] recTs;
     val newTs = Library.take (length (hd descr), recTs);
-    val T' = TFree (variant used "'t", HOLogic.typeS);
+    val T' = TFree (Name.variant used "'t", HOLogic.typeS);
 
     val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
@@ -319,7 +319,7 @@
     val recTs = get_rec_types descr' sorts;
     val used' = foldr add_typ_tfree_names [] recTs;
     val newTs = Library.take (length (hd descr), recTs);
-    val T' = TFree (variant used' "'t", HOLogic.typeS);
+    val T' = TFree (Name.variant used' "'t", HOLogic.typeS);
     val P = Free ("P", T' --> HOLogic.boolT);
 
     fun make_split (((_, (_, _, constrs)), T), comb_t) =
@@ -330,7 +330,7 @@
         fun process_constr (((cname, cargs), f), (t1s, t2s)) =
           let
             val Ts = map (typ_of_dtyp descr' sorts) cargs;
-            val frees = map Free (variantlist (make_tnames Ts, used) ~~ Ts);
+            val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);
             val eqn = HOLogic.mk_eq (Free ("x", T),
               list_comb (Const (cname, Ts ---> T), frees));
             val P' = P $ list_comb (f, frees)
@@ -437,7 +437,7 @@
         fun mk_clause ((f, g), (cname, _)) =
           let
             val (Ts, _) = strip_type (fastype_of f);
-            val tnames = variantlist (make_tnames Ts, used);
+            val tnames = Name.variant_list used (make_tnames Ts);
             val frees = map Free (tnames ~~ Ts)
           in
             list_all_free (tnames ~~ Ts, Logic.mk_implies
@@ -472,7 +472,7 @@
     fun mk_eqn T (cname, cargs) =
       let
         val Ts = map (typ_of_dtyp descr' sorts) cargs;
-        val tnames = variantlist (make_tnames Ts, ["v"]);
+        val tnames = Name.variant_list ["v"] (make_tnames Ts);
         val frees = tnames ~~ Ts
       in
         foldr (fn ((s, T'), t) => HOLogic.mk_exists (s, T', t))
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -63,7 +63,7 @@
       (fn (j, ((i, (_, _, constrs)), T)) => foldl_map (fn (j, (cname, cargs)) =>
         let
           val Ts = map (typ_of_dtyp descr sorts) cargs;
-          val tnames = variantlist (DatatypeProp.make_tnames Ts, pnames);
+          val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
           val recs = List.filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
           val frees = tnames ~~ Ts;
 
@@ -171,8 +171,7 @@
     fun make_casedist_prem T (cname, cargs) =
       let
         val Ts = map (typ_of_dtyp descr sorts) cargs;
-        val frees = variantlist
-          (DatatypeProp.make_tnames Ts, ["P", "y"]) ~~ Ts;
+        val frees = Name.variant_list ["P", "y"] (DatatypeProp.make_tnames Ts) ~~ Ts;
         val free_ts = map Free frees;
         val r = Free ("r" ^ NameSpace.base cname, Ts ---> rT)
       in (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -392,7 +392,7 @@
         fun mk_thm i =
           let
             val Ts = map (TFree o rpair HOLogic.typeS)
-              (variantlist (replicate i "'t", used));
+              (Name.variant_list used (replicate i "'t"));
             val f = Free ("f", Ts ---> U)
           in Goal.prove_global sign [] [] (Logic.mk_implies
             (HOLogic.mk_Trueprop (HOLogic.list_all
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Tools/function_package/fundef_prep.ML
--- a/src/HOL/Tools/function_package/fundef_prep.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 
-A package for general recursive function definitions. 
+A package for general recursive function definitions.
 Preparation step: makes auxiliary definitions and generates
 proof obligations.
 *)
@@ -10,20 +10,16 @@
 signature FUNDEF_PREP =
 sig
     val prepare_fundef : theory -> thm list -> string -> term -> FundefCommon.glrs -> string list
-			 -> FundefCommon.prep_result * theory
+                         -> FundefCommon.prep_result * theory
 
 end
 
-
-
-
-
 structure FundefPrep (*: FUNDEF_PREP*) =
 struct
 
 
 open FundefCommon
-open FundefAbbrev 
+open FundefAbbrev
 
 (* Theory dependencies. *)
 val Pair_inject = thm "Product_Type.Pair_inject";
@@ -39,30 +35,30 @@
 
 
 fun split_list3 [] = ([],[],[])
-  | split_list3 ((x,y,z)::xyzs) = 
+  | split_list3 ((x,y,z)::xyzs) =
     let
-	val (xs, ys, zs) = split_list3 xyzs
+        val (xs, ys, zs) = split_list3 xyzs
     in
-	(x::xs,y::ys,z::zs)
+        (x::xs,y::ys,z::zs)
     end
 
 
 fun build_tree thy f congs ctx (qs, gs, lhs, rhs) =
     let
-	(* FIXME: Save precomputed dependencies in a theory data slot *)
-	val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs)
+        (* FIXME: Save precomputed dependencies in a theory data slot *)
+        val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs)
 
-        val (_(*FIXME*), ctx') = ProofContext.add_fixes_i (map (fn Free (n, T) => (n, SOME T, NoSyn)) qs) ctx 
+        val (_(*FIXME*), ctx') = ProofContext.add_fixes_i (map (fn Free (n, T) => (n, SOME T, NoSyn)) qs) ctx
     in
-	FundefCtxTree.mk_tree thy congs_deps f ctx' rhs
+        FundefCtxTree.mk_tree thy congs_deps f ctx' rhs
     end
 
 
 fun find_calls tree =
     let
       fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs)
-	| add_Ri _ _ _ _ = raise Match
-    in                                 
+        | add_Ri _ _ _ _ = raise Match
+    in
       rev (FundefCtxTree.traverse_tree add_Ri tree [])
     end
 
@@ -71,68 +67,68 @@
 (* maps (qs,gs,lhs,ths) to (qs',gs',lhs',rhs') with primed variables *)
 fun mk_primed_vars thy glrs =
     let
-	val used = fold (fn (qs,_,_,_) => fold ((insert op =) o fst o dest_Free) qs) glrs []
+        val used = fold (fn (qs,_,_,_) => fold ((insert op =) o fst o dest_Free) qs) glrs []
 
-	fun rename_vars (qs,gs,lhs,rhs) =
-	    let
-		val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
-		val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
-	    in
-		(qs', map rename_vars gs, rename_vars lhs, rename_vars rhs)
-	    end
+        fun rename_vars (qs,gs,lhs,rhs) =
+            let
+                val qs' = map (fn Free (v,T) => Free (Name.variant used (v ^ "'"),T)) qs
+                val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
+            in
+                (qs', map rename_vars gs, rename_vars lhs, rename_vars rhs)
+            end
     in
-	map rename_vars glrs
+        map rename_vars glrs
     end
 
 
 
 (* Chooses fresh free names, declares G and R, defines f and returns a record
-   with all the information *)  
+   with all the information *)
 fun setup_context f glrs defname thy =
     let
-	val Const (f_fullname, fT) = f
-	val fname = Sign.base_name f_fullname
+        val Const (f_fullname, fT) = f
+        val fname = Sign.base_name f_fullname
 
-	val domT = domain_type fT 
-	val ranT = range_type fT
+        val domT = domain_type fT
+        val ranT = range_type fT
 
-	val GT = mk_relT (domT, ranT)
-	val RT = mk_relT (domT, domT)
-	val G_name = defname ^ "_graph"
-	val R_name = defname ^ "_rel"
+        val GT = mk_relT (domT, ranT)
+        val RT = mk_relT (domT, domT)
+        val G_name = defname ^ "_graph"
+        val R_name = defname ^ "_rel"
 
         val gfixes = [("h_fd", domT --> ranT),
-	              ("y_fd", ranT),
-	              ("x_fd", domT),
-	              ("z_fd", domT),
-	              ("a_fd", domT),
-	              ("D_fd", HOLogic.mk_setT domT),
-	              ("P_fd", domT --> boolT),
-	              ("Pb_fd", boolT),
-	              ("f_fd", fT)]
+                      ("y_fd", ranT),
+                      ("x_fd", domT),
+                      ("z_fd", domT),
+                      ("a_fd", domT),
+                      ("D_fd", HOLogic.mk_setT domT),
+                      ("P_fd", domT --> boolT),
+                      ("Pb_fd", boolT),
+                      ("f_fd", fT)]
 
         val (fxnames, ctx) = (ProofContext.init thy)
                                |> ProofContext.add_fixes_i (map (fn (n,T) => (n, SOME T, NoSyn)) gfixes)
 
         val [h, y, x, z, a, D, P, Pbool, fvar] = map (fn (n,(_,T)) => Free (n, T)) (fxnames ~~ gfixes)
-                                                                                    
+
         val Free (fvarname, _) = fvar
 
-	val glrs' = mk_primed_vars thy glrs
+        val glrs' = mk_primed_vars thy glrs
 
-	val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
+        val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
 
-	val G = Const (Sign.full_name thy G_name, GT)
-	val R = Const (Sign.full_name thy R_name, RT)
-	val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R
+        val G = Const (Sign.full_name thy G_name, GT)
+        val R = Const (Sign.full_name thy R_name, RT)
+        val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R
 
-	val f_eq = Logic.mk_equals (f $ x, 
-				    Const ("The", (ranT --> boolT) --> ranT) $
-					  Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
+        val f_eq = Logic.mk_equals (f $ x,
+                                    Const ("The", (ranT --> boolT) --> ranT) $
+                                          Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
 
-	val ([f_def], thy) = PureThy.add_defs_i false [((fname ^ "_def", f_eq), [])] thy
+        val ([f_def], thy) = PureThy.add_defs_i false [((fname ^ "_def", f_eq), [])] thy
     in
-	(Names {f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, ctx=ctx}, thy)
+        (Names {f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, ctx=ctx}, thy)
     end
 
 
@@ -142,8 +138,8 @@
 (* !!qs' qs. Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *)
 fun mk_compat_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) =
     (implies $ Trueprop (mk_eq (lhs, lhs'))
-	     $ Trueprop (mk_eq (rhs, rhs')))
-	|> fold_rev (curry Logic.mk_implies) (gs @ gs')
+             $ Trueprop (mk_eq (rhs, rhs')))
+        |> fold_rev (curry Logic.mk_implies) (gs @ gs')
         |> fold_rev mk_forall (qs @ qs')
 
 (* all proof obligations *)
@@ -153,35 +149,35 @@
 
 fun mk_completeness names glrs =
     let
-	val Names {domT, x, Pbool, ...} = names
+        val Names {domT, x, Pbool, ...} = names
 
-	fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
-						|> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
-						|> fold_rev (curry Logic.mk_implies) gs
-						|> fold_rev mk_forall qs
+        fun mk_case (qs, gs, lhs, _) = Trueprop Pbool
+                                                |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs)))
+                                                |> fold_rev (curry Logic.mk_implies) gs
+                                                |> fold_rev mk_forall qs
     in
-	Trueprop Pbool
-		 |> fold_rev (curry Logic.mk_implies o mk_case) glrs
+        Trueprop Pbool
+                 |> fold_rev (curry Logic.mk_implies o mk_case) glrs
                  |> mk_forall_rename (x, "x")
                  |> mk_forall_rename (Pbool, "P")
     end
 
 
-fun inductive_def_wrap defs (thy, const) = 
-    let 
+fun inductive_def_wrap defs (thy, const) =
+    let
       val qdefs = map dest_all_all defs
 
-      val (thy, {intrs = intrs_gen, elims = [elim_gen], ...}) = 
-	  InductivePackage.add_inductive_i true (*verbose*)
-					     false (*add_consts*)
-					     "" (* no altname *)
-					     false (* no coind *)
-					     false (* elims, please *)
-					     false (* induction thm please *)
-					     [const] (* the constant *)
-					     (map (fn (_,t) => (("", t),[])) qdefs) (* the intros *)
-					     [] (* no special monos *)
-					     thy
+      val (thy, {intrs = intrs_gen, elims = [elim_gen], ...}) =
+          InductivePackage.add_inductive_i true (*verbose*)
+                                             false (*add_consts*)
+                                             "" (* no altname *)
+                                             false (* no coind *)
+                                             false (* elims, please *)
+                                             false (* induction thm please *)
+                                             [const] (* the constant *)
+                                             (map (fn (_,t) => (("", t),[])) qdefs) (* the intros *)
+                                             [] (* no special monos *)
+                                             thy
 
 (* It would be nice if this worked... But this is actually HO-Unification... *)
 (*      fun inst (qs, intr) intr_gen =
@@ -191,7 +187,7 @@
                     |> fold_rev (forall_intr o cterm_of thy) qs*)
 
       fun inst (qs, intr) intr_gen =
-          intr_gen 
+          intr_gen
             |> Thm.freezeT
             |> fold_rev (forall_intr o (fn Free (n, T) => cterm_of thy (Var ((n,0), T)))) qs
 
@@ -208,10 +204,10 @@
 
 
 (*
- * "!!qs xs. CS ==> G => (r, lhs) : R" 
+ * "!!qs xs. CS ==> G => (r, lhs) : R"
  *)
 fun mk_RIntro R (qs, gs, lhs, rhs) (rcfix, rcassm, rcarg) =
-    mk_relmem (rcarg, lhs) R 
+    mk_relmem (rcarg, lhs) R
               |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
               |> fold_rev (curry Logic.mk_implies) gs
               |> fold_rev (mk_forall o Free) rcfix
@@ -236,32 +232,32 @@
 
 fun mk_clause_info thy names no (qs,gs,lhs,rhs) tree RCs GIntro_thm RIntro_thms =
     let
-	val Names {G, h, f, fvar, x, ...} = names 
-				 
-	val cqs = map (cterm_of thy) qs
-	val ags = map (assume o cterm_of thy) gs
+        val Names {G, h, f, fvar, x, ...} = names
+
+        val cqs = map (cterm_of thy) qs
+        val ags = map (assume o cterm_of thy) gs
 
         val used = [] (* XXX *)
                   (* FIXME: What is the relationship between this and mk_primed_vars? *)
-	val qs' = map (fn Free (v,T) => Free (variant used (v ^ "'"),T)) qs
-	val cqs' = map (cterm_of thy) qs'
+        val qs' = map (fn Free (v,T) => Free (Name.variant used (v ^ "'"),T)) qs
+        val cqs' = map (cterm_of thy) qs'
 
-	val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
-	val ags' = map (assume o cterm_of thy o rename_vars) gs
-	val lhs' = rename_vars lhs
-	val rhs' = rename_vars rhs
+        val rename_vars = Pattern.rewrite_term thy (qs ~~ qs') []
+        val ags' = map (assume o cterm_of thy o rename_vars) gs
+        val lhs' = rename_vars lhs
+        val rhs' = rename_vars rhs
 
         val lGI = GIntro_thm
                     |> forall_elim (cterm_of thy f)
                     |> fold forall_elim cqs
                     |> fold implies_elim_swp ags
-		
+
         (* FIXME: Can be removed when inductive-package behaves nicely. *)
-        val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) []) 
+        val ordcqs' = map (cterm_of thy o Pattern.rewrite_term thy ((fvar,h)::(qs ~~ qs')) [])
                           (term_frees (snd (dest_all_all (prop_of GIntro_thm))))
-               	  
-	fun mk_call_info (rcfix, rcassm, rcarg) RI =
-	    let
+
+        fun mk_call_info (rcfix, rcassm, rcarg) RI =
+            let
                 val crcfix = map (cterm_of thy o Free) rcfix
 
                 val llRI = RI
@@ -270,32 +266,32 @@
                              |> fold implies_elim_swp ags
                              |> fold implies_elim_swp rcassm
 
-                val h_assum = 
+                val h_assum =
                     mk_relmem (rcarg, h $ rcarg) G
                               |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
                               |> fold_rev (mk_forall o Free) rcfix
                               |> Pattern.rewrite_term thy [(f, h)] []
 
-		val Gh = assume (cterm_of thy h_assum)
-		val Gh' = assume (cterm_of thy (rename_vars h_assum))
-	    in
-		RCInfo {RIvs=rcfix, Gh=Gh, Gh'=Gh', rcarg=rcarg, CCas=rcassm, llRI=llRI}
-	    end
+                val Gh = assume (cterm_of thy h_assum)
+                val Gh' = assume (cterm_of thy (rename_vars h_assum))
+            in
+                RCInfo {RIvs=rcfix, Gh=Gh, Gh'=Gh', rcarg=rcarg, CCas=rcassm, llRI=llRI}
+            end
 
-	val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
+        val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs))))
 
         val RC_infos = map2 mk_call_info RCs RIntro_thms
     in
-	ClauseInfo
-	    {
-	     no=no,
-	     qs=qs, gs=gs, lhs=lhs, rhs=rhs,		 
-	     cqs=cqs, ags=ags,		 
-	     cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs', 
-	     lGI=lGI, RCs=RC_infos,
-	     tree=tree, case_hyp = case_hyp,
+        ClauseInfo
+            {
+             no=no,
+             qs=qs, gs=gs, lhs=lhs, rhs=rhs,
+             cqs=cqs, ags=ags,
+             cqs'=cqs', ags'=ags', lhs'=lhs', rhs'=rhs',
+             lGI=lGI, RCs=RC_infos,
+             tree=tree, case_hyp = case_hyp,
              ordcqs'=ordcqs'
-	    }
+            }
     end
 
 
@@ -311,9 +307,9 @@
 fun store_compat_thms 0 thms = []
   | store_compat_thms n thms =
     let
-	val (thms1, thms2) = chop n thms
+        val (thms1, thms2) = chop n thms
     in
-	(thms1 :: store_compat_thms (n - 1) thms2)
+        (thms1 :: store_compat_thms (n - 1) thms2)
     end
 
 
@@ -326,32 +322,32 @@
 (* Returns "Gsi, Gsj', lhs_i = lhs_j' |-- rhs_j'_f = rhs_i_f" *)
 (* if j < i, then turn around *)
 fun get_compat_thm thy cts clausei clausej =
-    let 
-	val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
-	val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
+    let
+        val ClauseInfo {no=i, cqs=qsi, ags=gsi, lhs=lhsi, ...} = clausei
+        val ClauseInfo {no=j, cqs'=qsj', ags'=gsj', lhs'=lhsj', ...} = clausej
 
-	val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))
+        val lhsi_eq_lhsj' = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))
     in if j < i then
-	   let 
-	       val compat = lookup_compat_thm j i cts
-	   in
-	       compat         (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *)
+           let
+               val compat = lookup_compat_thm j i cts
+           in
+               compat         (* "!!qj qi'. Gsj => Gsi' => lhsj = lhsi' ==> rhsj = rhsi'" *)
                 |> fold forall_elim (qsj' @ qsi) (* "Gsj' => Gsi => lhsj' = lhsi ==> rhsj' = rhsi" *)
-		|> fold implies_elim_swp gsj'
-		|> fold implies_elim_swp gsi
-		|> implies_elim_swp ((assume lhsi_eq_lhsj') RS sym) (* "Gsj', Gsi, lhsi = lhsj' |-- rhsj' = rhsi" *)
-	   end
+                |> fold implies_elim_swp gsj'
+                |> fold implies_elim_swp gsi
+                |> implies_elim_swp ((assume lhsi_eq_lhsj') RS sym) (* "Gsj', Gsi, lhsi = lhsj' |-- rhsj' = rhsi" *)
+           end
        else
-	   let
-	       val compat = lookup_compat_thm i j cts
-	   in
-	       compat        (* "!!qi qj'. Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
+           let
+               val compat = lookup_compat_thm i j cts
+           in
+               compat        (* "!!qi qj'. Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
                  |> fold forall_elim (qsi @ qsj') (* "Gsi => Gsj' => lhsi = lhsj' ==> rhsi = rhsj'" *)
-		 |> fold implies_elim_swp gsi
-		 |> fold implies_elim_swp gsj'
-		 |> implies_elim_swp (assume lhsi_eq_lhsj')
-		 |> (fn thm => thm RS sym) (* "Gsi, Gsj', lhsi = lhsj' |-- rhsj' = rhsi" *)
-	   end
+                 |> fold implies_elim_swp gsi
+                 |> fold implies_elim_swp gsj'
+                 |> implies_elim_swp (assume lhsi_eq_lhsj')
+                 |> (fn thm => thm RS sym) (* "Gsi, Gsj', lhsi = lhsj' |-- rhsj' = rhsi" *)
+           end
     end
 
 
@@ -359,29 +355,29 @@
 (* Generates the replacement lemma with primed variables. A problem here is that one should not do
 the complete requantification at the end to replace the variables. One should find a way to be more efficient
 here. *)
-fun mk_replacement_lemma thy (names:naming_context) ih_elim clause = 
-    let 
-	val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names 
-	val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
+fun mk_replacement_lemma thy (names:naming_context) ih_elim clause =
+    let
+        val Names {fvar, f, x, y, h, Pbool, G, ranT, domT, R, ...} = names
+        val ClauseInfo {qs,cqs,ags,lhs,rhs,cqs',ags',case_hyp, RCs, tree, ...} = clause
 
-	val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
+        val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
 
-	val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
-	val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs
-	val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs
+        val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
+        val h_assums = map (fn RCInfo {Gh, ...} => Gh) RCs
+        val h_assums' = map (fn RCInfo {Gh', ...} => Gh') RCs
 
-	val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
+        val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
 
-	val (eql, _) = FundefCtxTree.rewrite_by_tree thy f h ih_elim_case_inst (Ris ~~ h_assums) tree
+        val (eql, _) = FundefCtxTree.rewrite_by_tree thy f h ih_elim_case_inst (Ris ~~ h_assums) tree
 
-	val replace_lemma = (eql RS meta_eq_to_obj_eq)
-				|> implies_intr (cprop_of case_hyp)
-				|> fold_rev (implies_intr o cprop_of) h_assums
-				|> fold_rev (implies_intr o cprop_of) ags
-				|> fold_rev forall_intr cqs
-				|> fold forall_elim cqs'
-				|> fold implies_elim_swp ags'
-				|> fold implies_elim_swp h_assums'
+        val replace_lemma = (eql RS meta_eq_to_obj_eq)
+                                |> implies_intr (cprop_of case_hyp)
+                                |> fold_rev (implies_intr o cprop_of) h_assums
+                                |> fold_rev (implies_intr o cprop_of) ags
+                                |> fold_rev forall_intr cqs
+                                |> fold forall_elim cqs'
+                                |> fold implies_elim_swp ags'
+                                |> fold implies_elim_swp h_assums'
     in
       replace_lemma
     end
@@ -391,84 +387,84 @@
 
 fun mk_uniqueness_clause thy names compat_store clausei clausej RLj =
     let
-	val Names {f, h, y, ...} = names
-	val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei
-	val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
+        val Names {f, h, y, ...} = names
+        val ClauseInfo {no=i, lhs=lhsi, case_hyp, ...} = clausei
+        val ClauseInfo {no=j, ags'=gsj', lhs'=lhsj', rhs'=rhsj', RCs=RCsj, ordcqs'=ordcqs'j, ...} = clausej
 
-	val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj'
-	val compat = get_compat_thm thy compat_store clausei clausej
-	val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj
+        val rhsj'h = Pattern.rewrite_term thy [(f,h)] [] rhsj'
+        val compat = get_compat_thm thy compat_store clausei clausej
+        val Ghsj' = map (fn RCInfo {Gh', ...} => Gh') RCsj
 
-	val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
-	val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j'	*)
+        val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h))))
+        val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
 
-	val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h)))))
+        val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h)))))
     in
-	(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
+        (trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *)
         |> implies_elim RLj (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *)
-	|> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
-	|> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
-	|> implies_intr (cprop_of y_eq_rhsj'h)
-	|> implies_intr (cprop_of lhsi_eq_lhsj') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *)
-	|> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
-	|> implies_elim_swp eq_pairs
-	|> fold_rev (implies_intr o cprop_of) Ghsj' 
-	|> fold_rev (implies_intr o cprop_of) gsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
-	|> implies_intr (cprop_of eq_pairs)
-	|> fold_rev forall_intr ordcqs'j
+        |> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *)
+        |> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *)
+        |> implies_intr (cprop_of y_eq_rhsj'h)
+        |> implies_intr (cprop_of lhsi_eq_lhsj') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *)
+        |> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
+        |> implies_elim_swp eq_pairs
+        |> fold_rev (implies_intr o cprop_of) Ghsj'
+        |> fold_rev (implies_intr o cprop_of) gsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *)
+        |> implies_intr (cprop_of eq_pairs)
+        |> fold_rev forall_intr ordcqs'j
     end
 
 
 
 fun mk_uniqueness_case thy names ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei =
     let
-	val Names {x, y, G, fvar, f, ranT, ...} = names
-	val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
+        val Names {x, y, G, fvar, f, ranT, ...} = names
+        val ClauseInfo {lhs, rhs, qs, cqs, ags, case_hyp, lGI, RCs, ...} = clausei
 
-	val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
+        val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro
 
-	fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
+        fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case)
                                                             |> fold_rev (implies_intr o cprop_of) CCas
-						            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
+                                                            |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
 
-	val existence = lGI (*|> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])*)
-			    |> fold (curry op COMP o prep_RC) RCs 
+        val existence = lGI (*|> instantiate ([], [(cterm_of thy (free_to_var fvar), cterm_of thy f)])*)
+                            |> fold (curry op COMP o prep_RC) RCs
 
-	val a = cterm_of thy (mk_prod (lhs, y))
-	val P = cterm_of thy (mk_eq (y, rhs))
-	val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G))))
+        val a = cterm_of thy (mk_prod (lhs, y))
+        val P = cterm_of thy (mk_eq (y, rhs))
+        val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G))))
 
-	val unique_clauses = map2 (mk_uniqueness_clause thy names compat_store clausei) clauses rep_lemmas
+        val unique_clauses = map2 (mk_uniqueness_clause thy names compat_store clausei) clauses rep_lemmas
 
-	val uniqueness = G_cases 
+        val uniqueness = G_cases
                            |> forall_elim a
                            |> forall_elim P
-			   |> implies_elim_swp a_in_G
-			   |> fold implies_elim_swp unique_clauses
-			   |> implies_intr (cprop_of a_in_G)
-			   |> forall_intr (cterm_of thy y) 
+                           |> implies_elim_swp a_in_G
+                           |> fold implies_elim_swp unique_clauses
+                           |> implies_intr (cprop_of a_in_G)
+                           |> forall_intr (cterm_of thy y)
 
-	val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *)
+        val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *)
 
-	val exactly_one =
-	    ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhs)]
-		 |> curry (op COMP) existence
-		 |> curry (op COMP) uniqueness
-		 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
-		 |> implies_intr (cprop_of case_hyp) 
-		 |> fold_rev (implies_intr o cprop_of) ags
-		 |> fold_rev forall_intr cqs
+        val exactly_one =
+            ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhs)]
+                 |> curry (op COMP) existence
+                 |> curry (op COMP) uniqueness
+                 |> simplify (HOL_basic_ss addsimps [case_hyp RS sym])
+                 |> implies_intr (cprop_of case_hyp)
+                 |> fold_rev (implies_intr o cprop_of) ags
+                 |> fold_rev forall_intr cqs
 
-	val function_value =
-	    existence 
-		|> fold_rev (implies_intr o cprop_of) ags
-		|> implies_intr ihyp
-		|> implies_intr (cprop_of case_hyp)
-		|> forall_intr (cterm_of thy x)
-		|> forall_elim (cterm_of thy lhs)
-		|> curry (op RS) refl
+        val function_value =
+            existence
+                |> fold_rev (implies_intr o cprop_of) ags
+                |> implies_intr ihyp
+                |> implies_intr (cprop_of case_hyp)
+                |> forall_intr (cterm_of thy x)
+                |> forall_elim (cterm_of thy lhs)
+                |> curry (op RS) refl
     in
-	(exactly_one, function_value)
+        (exactly_one, function_value)
     end
 
 
@@ -476,45 +472,45 @@
 
 fun prove_stuff thy congs names clauses complete compat compat_store G_elim R_elim =
     let
-	val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, Pbool, ...}:naming_context = names
+        val Names {G, R, acc_R, domT, ranT, f, f_def, x, z, fvarname, Pbool, ...}:naming_context = names
+
+        val f_def_fr = Thm.freezeT f_def
 
-	val f_def_fr = Thm.freezeT f_def
+        val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)]
+                                                [SOME (cterm_of thy f), SOME (cterm_of thy G)])
+                                      #> curry op COMP (forall_intr_vars f_def_fr)
 
-	val instantiate_and_def = (instantiate' [SOME (ctyp_of thy domT), SOME (ctyp_of thy ranT)] 
-						[SOME (cterm_of thy f), SOME (cterm_of thy G)])
-				      #> curry op COMP (forall_intr_vars f_def_fr)
-			  
-	val inst_ex1_ex = instantiate_and_def ex1_implies_ex
-	val inst_ex1_un = instantiate_and_def ex1_implies_un
-	val inst_ex1_iff = instantiate_and_def ex1_implies_iff
+        val inst_ex1_ex = instantiate_and_def ex1_implies_ex
+        val inst_ex1_un = instantiate_and_def ex1_implies_un
+        val inst_ex1_iff = instantiate_and_def ex1_implies_iff
+
+        (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
+        val ihyp = all domT $ Abs ("z", domT,
+                                   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
+                                           $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
+                                                             Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G)))
+                       |> cterm_of thy
 
-	(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
-	val ihyp = all domT $ Abs ("z", domT, 
-				   implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R)
-					   $ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $
-							     Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G)))
-		       |> cterm_of thy
-		   
-	val ihyp_thm = assume ihyp |> forall_elim_vars 0
-	val ih_intro = ihyp_thm RS inst_ex1_ex
-	val ih_elim = ihyp_thm RS inst_ex1_un
+        val ihyp_thm = assume ihyp |> forall_elim_vars 0
+        val ih_intro = ihyp_thm RS inst_ex1_ex
+        val ih_elim = ihyp_thm RS inst_ex1_un
 
-	val _ = Output.debug "Proving Replacement lemmas..."
-	val repLemmas = map (mk_replacement_lemma thy names ih_elim) clauses
+        val _ = Output.debug "Proving Replacement lemmas..."
+        val repLemmas = map (mk_replacement_lemma thy names ih_elim) clauses
+
+        val _ = Output.debug "Proving cases for unique existence..."
+        val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
 
-	val _ = Output.debug "Proving cases for unique existence..."
-	val (ex1s, values) = split_list (map (mk_uniqueness_case thy names ihyp ih_intro G_elim compat_store clauses repLemmas) clauses)
-
-	val _ = Output.debug "Proving: Graph is a function" (* FIXME: Rewrite this proof. *)
-	val graph_is_function = complete 
+        val _ = Output.debug "Proving: Graph is a function" (* FIXME: Rewrite this proof. *)
+        val graph_is_function = complete
                                   |> forall_elim_vars 0
-				  |> fold (curry op COMP) ex1s
-				  |> implies_intr (ihyp)
-				  |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, acc_R))))
-				  |> forall_intr (cterm_of thy x)
-				  |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
+                                  |> fold (curry op COMP) ex1s
+                                  |> implies_intr (ihyp)
+                                  |> implies_intr (cterm_of thy (Trueprop (mk_mem (x, acc_R))))
+                                  |> forall_intr (cterm_of thy x)
+                                  |> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
                                   |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
-				  |> Drule.close_derivation
+                                  |> Drule.close_derivation
 
         val goal = complete COMP (graph_is_function COMP conjunctionI)
                             |> Drule.close_derivation
@@ -539,9 +535,9 @@
 fun prepare_fundef thy congs defname f qglrs used =
     let
       val (names, thy) = setup_context f qglrs defname thy
-      val Names {G, R, ctx, glrs', fvar, ...} = names 
+      val Names {G, R, ctx, glrs', fvar, ...} = names
 
-                         
+
       val n = length qglrs
       val trees = map (build_tree thy f congs ctx) qglrs
       val RCss = map find_calls trees
@@ -558,16 +554,16 @@
 
       val R_intross = map2 (fn qglr => map (mk_RIntro R qglr)) qglrs RCss
       val G_intros = map2 (mk_GIntro thy f fvar G) qglrs RCss
-                    
+
       val (GIntro_thms, (thy, _, G_elim)) = inductive_def_wrap G_intros (thy, G)
       val (RIntro_thmss, (thy, _, R_elim)) = fold_burrow inductive_def_wrap R_intross (thy, R)
- 
+
       val clauses = map6 (mk_clause_info thy names) (1 upto n) qglrs trees RCss GIntro_thms RIntro_thmss
-                  
+
       val (goal, goalI, ex1_iff, values) = prove_stuff thy congs names clauses complete compat compat_store G_elim R_elim
     in
-	(Prep {names = names, goal = goal, goalI = goalI, values = values, clauses = clauses, ex1_iff = ex1_iff, R_cases = R_elim},
-	 thy) 
+        (Prep {names = names, goal = goal, goalI = goalI, values = values, clauses = clauses, ex1_iff = ex1_iff, R_cases = R_elim},
+         thy)
     end
 
 
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -343,7 +343,7 @@
 
 fun mk_v ((names, vs), s) = (case AList.lookup (op =) vs s of
       NONE => ((names, (s, [s])::vs), s)
-    | SOME xs => let val s' = variant names s in
+    | SOME xs => let val s' = Name.variant names s in
         ((s'::names, AList.update (op =) (s, s'::xs) vs), s') end);
 
 fun distinct_v (nvs, Var ((s, 0), T)) =
@@ -407,7 +407,7 @@
 
     fun check_constrt ((names, eqs), t) =
       if is_constrt thy t then ((names, eqs), t) else
-        let val s = variant names "x";
+        let val s = Name.variant names "x";
         in ((s::names, (s, t)::eqs), Var ((s, 0), fastype_of t)) end;
 
     fun compile_eq (gr, (s, t)) =
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Tools/inductive_package.ML
--- 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          *)
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -35,7 +35,7 @@
 fun strip_all t =
   let
     fun strip used (Const ("all", _) $ Abs (s, T, t)) =
-          let val s' = variant used s
+          let val s' = Name.variant used s
           in strip (s'::used) (subst_bound (Free (s', T), t)) end
       | strip used ((t as Const ("==>", _) $ P) $ Q) = t $ strip used Q
       | strip _ t = t;
@@ -152,7 +152,7 @@
     fun fun_of ts rts args used (prem :: prems) =
           let
             val T = Extraction.etype_of thy vs [] prem;
-            val [x, r] = variantlist (["x", "r"], used)
+            val [x, r] = Name.variant_list used ["x", "r"]
           in if T = Extraction.nullT
             then fun_of ts rts args used prems
             else if is_rec prem then
@@ -248,7 +248,7 @@
     handle DatatypeAux.Datatype_Empty name' =>
       let
         val name = Sign.base_name name';
-        val dname = variant used "Dummy"
+        val dname = Name.variant used "Dummy"
       in
         thy
         |> add_dummies f (map (add_dummy name dname) dts) (dname :: used)
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -1315,7 +1315,7 @@
     val fieldTs = (map snd fields);
     val alphas_zeta = alphas@[zeta];
     val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta;
-    val vT = TFree (variant alphas_zeta "'v", HOLogic.typeS);
+    val vT = TFree (Name.variant alphas_zeta "'v", HOLogic.typeS);
     val extT_name = suffix ext_typeN name
     val extT = Type (extT_name, alphas_zetaTs);
     val repT = foldr1 HOLogic.mk_prodT (fieldTs@[moreT]);
@@ -1385,8 +1385,8 @@
     val ext = mk_ext vars_more;
     val s     = Free (rN, extT);
     val w     = Free (wN, extT);
-    val P = Free (variant variants "P", extT-->HOLogic.boolT);
-    val C = Free (variant variants "C", HOLogic.boolT);
+    val P = Free (Name.variant variants "P", extT-->HOLogic.boolT);
+    val C = Free (Name.variant variants "C", HOLogic.boolT);
 
     val inject_prop =
       let val vars_more' = map (fn (Free (x,T)) => Free (x ^ "'",T)) vars_more;
@@ -1411,7 +1411,7 @@
 
     (*updates*)
     fun mk_upd_prop (i,(c,T)) =
-      let val x' = Free (variant variants (base c ^ "'"),T)
+      let val x' = Free (Name.variant variants (base c ^ "'"),T)
           val args' = nth_update (i, x') vars_more
       in mk_upd updN c x' ext === mk_ext args'  end;
     val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
@@ -1422,7 +1422,7 @@
       in s === mk_ext args end;
 
     val split_meta_prop =
-      let val P = Free (variant variants "P", extT-->Term.propT) in
+      let val P = Free (Name.variant variants "P", extT-->Term.propT) in
         Logic.mk_equals
          (All [dest_Free s] (P $ s), All (map dest_Free vars_more) (P $ ext))
       end;
@@ -1479,7 +1479,7 @@
     fun upd_convs_prf_opt () =
       let
         fun mkrefl (c,T) = Thm.reflexive
-                            (cterm_of defs_thy (Free (variant variants (base c ^ "'"),T)));
+                            (cterm_of defs_thy (Free (Name.variant variants (base c ^ "'"),T)));
         val refls = map mkrefl fields_more;
         val constr_refl = Thm.reflexive (cterm_of defs_thy (head_of ext));
         val dest_convs' = map mk_meta_eq dest_convs;
@@ -1595,7 +1595,7 @@
     val parent_names = map fst parent_fields;
     val parent_types = map snd parent_fields;
     val parent_fields_len = length parent_fields;
-    val parent_variants = variantlist (map base parent_names, [moreN, rN, rN ^ "'", wN]);
+    val parent_variants = Name.variant_list [moreN, rN, rN ^ "'", wN] (map base parent_names);
     val parent_vars = ListPair.map Free (parent_variants, parent_types);
     val parent_len = length parents;
     val parents_idx = (map #name parents) ~~ (0 upto (parent_len - 1));
@@ -1607,7 +1607,7 @@
     val alphas_fields = foldr add_typ_tfree_names [] types;
     val alphas_ext = alphas inter alphas_fields;
     val len = length fields;
-    val variants = variantlist (map fst bfields, moreN::rN::rN ^ "'"::wN::parent_variants);
+    val variants = Name.variant_list (moreN::rN::rN ^ "'"::wN::parent_variants) (map fst bfields);
     val vars = ListPair.map Free (variants, types);
     val named_vars = names ~~ vars;
     val idxs = 0 upto (len - 1);
@@ -1622,7 +1622,7 @@
     val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
 
 
-    val zeta = variant alphas "'z";
+    val zeta = Name.variant alphas "'z";
     val moreT = TFree (zeta, HOLogic.typeS);
     val more = Free (moreN, moreT);
     val full_moreN = full moreN;
@@ -1779,9 +1779,9 @@
 
     (* prepare propositions *)
     val _ = timing_msg "record preparing propositions";
-    val P = Free (variant all_variants "P", rec_schemeT0-->HOLogic.boolT);
-    val C = Free (variant all_variants "C", HOLogic.boolT);
-    val P_unit = Free (variant all_variants "P", recT0-->HOLogic.boolT);
+    val P = Free (Name.variant all_variants "P", rec_schemeT0-->HOLogic.boolT);
+    val C = Free (Name.variant all_variants "C", HOLogic.boolT);
+    val P_unit = Free (Name.variant all_variants "P", recT0-->HOLogic.boolT);
 
     (*selectors*)
     val sel_conv_props =
@@ -1789,7 +1789,7 @@
 
     (*updates*)
     fun mk_upd_prop (i,(c,T)) =
-      let val x' = Free (variant all_variants (base c ^ "'"),T)
+      let val x' = Free (Name.variant all_variants (base c ^ "'"),T)
           val args' = nth_update (parent_fields_len + i, x') all_vars_more
       in mk_upd updateN c x' r_rec0 === mk_rec args' 0  end;
     val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
@@ -1819,7 +1819,7 @@
 
     (*split*)
     val split_meta_prop =
-      let val P = Free (variant all_variants "P", rec_schemeT0-->Term.propT) in
+      let val P = Free (Name.variant all_variants "P", rec_schemeT0-->Term.propT) in
         Logic.mk_equals
          (All [dest_Free r0] (P $ r0), All (map dest_Free all_vars_more) (P $ r_rec0))
       end;
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -145,7 +145,7 @@
 	    end
 	| dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) (n, thx) =
 	    (*Universal quant: insert a free variable into body and continue*)
-	    let val fname = variant (add_term_names (p,[])) a
+	    let val fname = Name.variant (add_term_names (p,[])) a
 	    in dec_sko (subst_bound (Free(fname,T), p)) (n, thx) end
 	| dec_sko (Const ("op &", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy)
 	| dec_sko (Const ("op |", _) $ p $ q) nthy = dec_sko q (dec_sko p nthy)
@@ -157,7 +157,7 @@
 fun assume_skofuns th =
   let fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
 	    (*Existential: declare a Skolem function, then insert into body and continue*)
-	    let val name = variant (add_term_names (p,[])) (gensym "sko_")
+	    let val name = Name.variant (add_term_names (p,[])) (gensym "sko_")
                 val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
 		val args = term_frees xtp \\ skos  (*the formal parameters*)
 		val Ts = map type_of args
@@ -172,7 +172,7 @@
 	    end
 	| dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) defs =
 	    (*Universal quant: insert a free variable into body and continue*)
-	    let val fname = variant (add_term_names (p,[])) a
+	    let val fname = Name.variant (add_term_names (p,[])) a
 	    in dec_sko (subst_bound (Free(fname,T), p)) defs end
 	| dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
 	| dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOL/Tools/split_rule.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -81,7 +81,7 @@
         fun mk_tuple (v as Var ((a, _), T)) (xs, insts) =
               let
                 val Ts = HOLogic.prodT_factors T;
-                val ys = Term.variantlist (replicate (length Ts) a, xs);
+                val ys = Name.variant_list xs (replicate (length Ts) a);
               in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple T
                 (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
               end
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOLCF/domain/theorems.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -476,7 +476,7 @@
           val arg1 = (con1, args1);
           val arg2 =
             (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg)
-              (args2, variantlist (map vname args2,map vname args1)));
+              (args2, Name.variant_list (map vname args1) (map vname args2)));
         in [dist arg1 arg2, dist arg2 arg1] end;
     fun distincts []      = []
       | distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/HOLCF/fixrec_package.ML
--- a/src/HOLCF/fixrec_package.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/HOLCF/fixrec_package.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -142,7 +142,7 @@
       in pre_build f rhs' (v::vs) taken' end
   | Const(c,T) =>
       let
-        val n = variant taken "v";
+        val n = Name.variant taken "v";
         fun result_type (Type("Cfun.->",[_,T])) (x::xs) = result_type T xs
           | result_type T _ = T;
         val v = Free(n, result_type T vs);
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/Provers/IsaPlanner/isand.ML
--- a/src/Provers/IsaPlanner/isand.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Provers/IsaPlanner/isand.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -204,7 +204,7 @@
       val tvars = List.foldr Term.add_term_tvars [] ts;
       val (names',renamings) = 
           List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => 
-                         let val n2 = Term.variant Ns n in 
+                         let val n2 = Name.variant Ns n in 
                            (n2::Ns, (tv, (n2,s))::Rs)
                          end) (tfree_names @ names,[]) tvars;
     in renamings end;
@@ -237,7 +237,7 @@
       val Ns = List.foldr Term.add_term_names names ts;
       val (_,renamings) = 
           Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
-                    let val n2 = Term.variant Ns n in
+                    let val n2 = Name.variant Ns n in
                       (n2 :: Ns, (v, (n2,ty)) :: Rs)
                     end) ((Ns,[]), vars);
     in renamings end;
@@ -436,7 +436,7 @@
       val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
       val names = Term.add_term_names (t,varnames);
       val fvs = map Free 
-                    ((Term.variantlist (map fst alls, names)) 
+                    (Name.variant_list names (map fst alls)
                        ~~ (map snd alls));
     in ((subst_bounds (fvs,t)), fvs) end;
 
@@ -448,7 +448,7 @@
       val body = Term.strip_all_body gt;
       val alls = rev (Term.strip_all_vars gt);
       val fvs = map Free 
-                    ((Term.variantlist (map fst alls, names)) 
+                    (Name.variant_list names (map fst alls)
                        ~~ (map snd alls));
     in ((subst_bounds (fvs,body)), fvs) end;
 
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/Provers/IsaPlanner/rw_inst.ML
--- a/src/Provers/IsaPlanner/rw_inst.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Provers/IsaPlanner/rw_inst.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -109,7 +109,7 @@
       val names = usednames_of_thm rule;
       val (fromnames,tonames,names2,Ts') = 
           Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => 
-                    let val n2 = Term.variant names n in
+                    let val n2 = Name.variant names n in
                       (ctermify (Free(faken,ty)) :: rnf,
                        ctermify (Free(n2,ty)) :: rnt, 
                        n2 :: names,
@@ -156,7 +156,7 @@
       val vars_to_fix = Library.union (termvars, cond_vs);
       val (renamings, names2) = 
           foldr (fn (((n,i),ty), (vs, names')) => 
-                    let val n' = Term.variant names' n in
+                    let val n' = Name.variant names' n in
                       ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
                     end)
                 ([], names) vars_to_fix;
@@ -164,7 +164,7 @@
 
 (* make a new fresh typefree instantiation for the given tvar *)
 fun new_tfree (tv as (ix,sort), (pairs,used)) =
-      let val v = variant used (string_of_indexname ix)
+      let val v = Name.variant used (string_of_indexname ix)
       in  ((ix,(sort,TFree(v,sort)))::pairs, v::used)  end;
 
 
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/Provers/eqsubst.ML
--- a/src/Provers/eqsubst.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Provers/eqsubst.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -180,7 +180,7 @@
 fun fakefree_badbounds Ts t = 
     let val (FakeTs,Ts,newnames) = 
             List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
-                           let val newname = Term.variant usednames n
+                           let val newname = Name.variant usednames n
                            in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
                                (newname,ty)::Ts, 
                                newname::usednames) end)
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/Pure/Proof/proofchecker.ML
--- a/src/Pure/Proof/proofchecker.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Pure/Proof/proofchecker.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -62,7 +62,7 @@
 
       | thm_of vs Hs (Abst (s, SOME T, prf)) =
           let
-            val x = variant (names @ map fst vs) s;
+            val x = Name.variant (names @ map fst vs) s;
             val thm = thm_of ((x, T) :: vs) Hs prf
           in
             Thm.forall_intr (Thm.cterm_of sg (Free (x, T))) thm
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -370,7 +370,7 @@
 
 fun invent seed used =
   let
-    val x = Term.variant used seed
+    val x = Name.variant used seed
   in (x, x :: used) end;
 
 fun eta_expand (c as (_, (_, ty)), es) k =
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Pure/codegen.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -337,7 +337,7 @@
 
 fun preprocess_term thy t =
   let
-    val x = Free (variant (add_term_names (t, [])) "x", fastype_of t);
+    val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t);
     (* fake definition *)
     val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
       (Logic.mk_equals (x, t));
@@ -539,7 +539,7 @@
     val (illegal, alt_names) = split_list (map_filter (fn s =>
       let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names)
     val ps = (reserved @ illegal) ~~
-      variantlist (map (suffix "'") reserved @ alt_names, names);
+      Name.variant_list names (map (suffix "'") reserved @ alt_names);
 
     fun rename_id s = AList.lookup (op =) ps s |> the_default s;
 
@@ -688,9 +688,9 @@
          separate (Pretty.brk 1) (p :: ps) @ [Pretty.str ")"])
      else Pretty.block (separate (Pretty.brk 1) (p :: ps));
 
-fun new_names t xs = variantlist (map mk_id xs,
-  map (fst o fst o dest_Var) (term_vars t) union
-  add_term_names (t, ThmDatabase.ml_reserved));
+fun new_names t xs = Name.variant_list
+  (map (fst o fst o dest_Var) (term_vars t) union
+    add_term_names (t, ThmDatabase.ml_reserved)) (map mk_id xs);
 
 fun new_name t x = hd (new_names t [x]);
 
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Pure/proofterm.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -568,8 +568,8 @@
             (([], [], [], []), prf);
     val fs' = map (fst o dest_Free) fs;
     val vs' = map (fst o dest_Var) vs;
-    val names = vs' ~~ variantlist (map fst vs', fs');
-    val names' = Tvs ~~ variantlist (map fst Tvs, Tfs);
+    val names = vs' ~~ Name.variant_list fs' (map fst vs');
+    val names' = Tvs ~~ Name.variant_list Tfs (map fst Tvs);
     val rnames = map swap names;
     val rnames' = map swap names';
   in
@@ -607,7 +607,7 @@
     val fs = Term.fold_types (Term.fold_atyps
       (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
     val ixns = add_term_tvar_ixns (t, []);
-    val fmap = fs ~~ variantlist (map fst fs, map #1 ixns)
+    val fmap = fs ~~ Name.variant_list (map #1 ixns) (map fst fs)
     fun thaw (f as (a, S)) =
       (case AList.lookup (op =) fmap f of
         NONE => TFree f
@@ -619,7 +619,7 @@
 local
 
 fun new_name (ix, (pairs,used)) =
-  let val v = variant used (string_of_indexname ix)
+  let val v = Name.variant used (string_of_indexname ix)
   in  ((ix, v) :: pairs, v :: used)  end;
 
 fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Pure/pure_thy.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -441,7 +441,7 @@
       (fn Var ((x, j), _) => if i = j then curry (op ins_string) x else I | _ => I);
     val used = fold (fn (t, u) => add_used t o add_used u) tpairs (add_used prop []);
     val vars = strip_vars prop;
-    val cvars = (Term.variantlist (map #1 vars, used), vars)
+    val cvars = (Name.variant_list used (map #1 vars), vars)
       |> ListPair.map (fn (x, (_, T)) => Thm.cterm_of thy (Var ((x, i), T)));
   in fold Thm.forall_elim cvars th end;
 
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Pure/thm.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -1343,7 +1343,7 @@
     val short = length iparams - length cs;
     val newnames =
       if short < 0 then error "More names than abstractions!"
-      else variantlist (Library.take (short, iparams), cs) @ cs;
+      else Name.variant_list cs (Library.take (short, iparams)) @ cs;
     val freenames = map (#1 o dest_Free) (term_frees Bi);
     val newBi = Logic.list_rename_params (newnames, Bi);
   in
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/Pure/type.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -233,7 +233,7 @@
     val fs = Term.fold_types (Term.fold_atyps
       (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
     val ixns = add_term_tvar_ixns (t, []);
-    val fmap = fs ~~ map (rpair 0) (variantlist (map fst fs, map #1 ixns))
+    val fmap = fs ~~ map (rpair 0) (Name.variant_list (map #1 ixns) (map fst fs))
     fun thaw (f as (a, S)) =
       (case AList.lookup (op =) fmap f of
         NONE => TFree f
@@ -246,7 +246,7 @@
 local
 
 fun new_name (ix, (pairs, used)) =
-  let val v = variant used (string_of_indexname ix)
+  let val v = Name.variant used (string_of_indexname ix)
   in ((ix, v) :: pairs, v :: used) end;
 
 fun freeze_one alist (ix, sort) =
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -100,7 +100,7 @@
                Sign.string_of_term sign t);
 
   (*** Construct the fixedpoint definition ***)
-  val mk_variant = variant (foldr add_term_names [] intr_tms);
+  val mk_variant = Name.variant (foldr add_term_names [] intr_tms);
 
   val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
 
diff -r 3f31fb81b83a -r 8f3e1ddb50e6 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Tue Jul 11 12:16:52 2006 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Tue Jul 11 12:16:54 2006 +0200
@@ -147,7 +147,7 @@
     (** make definition **)
 
     (*the recursive argument*)
-    val rec_arg = Free (variant (map #1 (ls@rs)) (Sign.base_name big_rec_name),
+    val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Sign.base_name big_rec_name),
                         Ind_Syntax.iT)
 
     val def_tm = Logic.mk_equals