diff -r 257e01fab4b7 -r c1f0bc7e7d80 src/HOL/ex/reflection.ML
--- a/src/HOL/ex/reflection.ML	Sat Sep 30 20:54:34 2006 +0200
+++ b/src/HOL/ex/reflection.ML	Sat Sep 30 21:39:17 2006 +0200
@@ -39,7 +39,7 @@
        if (fN mem (term_consts t)) then (fn _ => [t]) else (fn _ => [])
      | add_fterms _ = I
    val fterms = add_fterms rhs []
-   val (xs, ctxt'') = Variable.invent_fixes (replicate (length fterms) "x") ctxt'
+   val (xs, ctxt'') = Variable.variant_fixes (replicate (length fterms) "x") ctxt'
    val tys = map fastype_of fterms
    val vs = map Free (xs ~~ tys)
    val env = fterms ~~ vs
@@ -111,7 +111,7 @@
    (case s of 
      Abs(xn,xT,ta) => 
      (let
-       val ([xn],ctxt') = Variable.invent_fixes ["x"] ctxt
+       val ([xn],ctxt') = Variable.variant_fixes ["x"] ctxt
        val (xn,ta) = variant_abs (xn,xT,ta)
        val x = Free(xn,xT)
        val _ = (case AList.lookup (op =) (!bds) (HOLogic.listT xT)
@@ -164,7 +164,7 @@
    | t1$t2 => (get_nth t1 handle REIF "get_nth" => get_nth t2)
    | Abs(_,_,t') => get_nth t'
    | _ => raise REIF "get_nth"
-  val ([xn,vsn],ctxt') = Variable.invent_fixes ["x","vs"] ctxt
+  val ([xn,vsn],ctxt') = Variable.variant_fixes ["x","vs"] ctxt
   val thy = ProofContext.theory_of ctxt'
   val cert = cterm_of thy
   fun tryeqs [] = raise REIF "Can not find the atoms equation"
@@ -213,7 +213,7 @@
      ([],
       fn ths =>
         let 
-         val ([x], ctxt') = Variable.invent_fixes ["vs"] ctxt
+         val ([x], ctxt') = Variable.variant_fixes ["vs"] ctxt
 	 val cert = cterm_of (ProofContext.theory_of ctxt')
          val (Const("List.nth",_)$(vs as Var((vsn,vsi),_))$n) = 
              (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th
@@ -239,7 +239,7 @@
   val tys = foldr (fn (f,ts) => (f |> fastype_of |> binder_types |> split_last |> fst) 
 				    union ts) [] fs
   val _ = bds := AList.make (fn _ => ([],[])) tys
-  val (vs, ctxt') = Variable.invent_fixes (replicate (length tys) "vs") ctxt
+  val (vs, ctxt') = Variable.variant_fixes (replicate (length tys) "vs") ctxt
   val thy = ProofContext.theory_of ctxt'
   val cert = cterm_of thy
   val vstys = map (fn (t,v) => (t,SOME (cert (Free(v,t))))) 
@@ -301,4 +301,4 @@
             val th = (genreflect ctxt corr_thm raw_eqs t) RS ssubst
         in rtac th i st end);
 
-end
\ No newline at end of file
+end