# HG changeset patch
# User wenzelm
# Date 1159645157 -7200
# Node ID c1f0bc7e7d80db0f5bde68b51e85144dc5ab2f0a
# Parent  257e01fab4b7ffbf5b3ed2f5b4587102d079e99b
renamed Variable.invent_fixes to Variable.variant_fixes;

diff -r 257e01fab4b7 -r c1f0bc7e7d80 doc-src/IsarImplementation/Thy/document/proof.tex
--- a/doc-src/IsarImplementation/Thy/document/proof.tex	Sat Sep 30 20:54:34 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Sat Sep 30 21:39:17 2006 +0200
@@ -106,7 +106,7 @@
 \begin{mldecls}
   \indexml{Variable.add-fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
 \verb|  string list -> Proof.context -> string list * Proof.context| \\
-  \indexml{Variable.invent-fixes}\verb|Variable.invent_fixes: |\isasep\isanewline%
+  \indexml{Variable.variant-fixes}\verb|Variable.variant_fixes: |\isasep\isanewline%
 \verb|  string list -> Proof.context -> string list * Proof.context| \\
   \indexml{Variable.declare-term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
   \indexml{Variable.declare-constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
@@ -126,7 +126,7 @@
   already.  There is a different policy within a local proof body: the
   given names are just hints for newly invented Skolem variables.
 
-  \item \verb|Variable.invent_fixes| is similar to \verb|Variable.add_fixes|, but always produces fresh variants of the given
+  \item \verb|Variable.variant_fixes| is similar to \verb|Variable.add_fixes|, but always produces fresh variants of the given
   names.
 
   \item \verb|Variable.declare_term|~\isa{t\ ctxt} declares term
diff -r 257e01fab4b7 -r c1f0bc7e7d80 doc-src/IsarImplementation/Thy/proof.thy
--- a/doc-src/IsarImplementation/Thy/proof.thy	Sat Sep 30 20:54:34 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy	Sat Sep 30 21:39:17 2006 +0200
@@ -88,7 +88,7 @@
   \begin{mldecls}
   @{index_ML Variable.add_fixes: "
   string list -> Proof.context -> string list * Proof.context"} \\
-  @{index_ML Variable.invent_fixes: "
+  @{index_ML Variable.variant_fixes: "
   string list -> Proof.context -> string list * Proof.context"} \\
   @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\
   @{index_ML Variable.declare_constraints: "term -> Proof.context -> Proof.context"} \\
@@ -108,7 +108,7 @@
   already.  There is a different policy within a local proof body: the
   given names are just hints for newly invented Skolem variables.
 
-  \item @{ML Variable.invent_fixes} is similar to @{ML
+  \item @{ML Variable.variant_fixes} is similar to @{ML
   Variable.add_fixes}, but always produces fresh variants of the given
   names.
 
diff -r 257e01fab4b7 -r c1f0bc7e7d80 src/HOL/Tools/function_package/fundef_prep.ML
--- a/src/HOL/Tools/function_package/fundef_prep.ML	Sat Sep 30 20:54:34 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_prep.ML	Sat Sep 30 21:39:17 2006 +0200
@@ -84,7 +84,7 @@
 
 fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
     let
-      val (qs, ctxt') = Variable.invent_fixes (map fst pre_qs) ctxt
+      val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
                                            |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
 
       val thy = ProofContext.theory_of ctxt'
@@ -458,7 +458,7 @@
 fun fix_globals domT ranT fvar ctxt =
     let
       val ([h, y, x, z, a, D, P, Pbool],ctxt') = 
-          Variable.invent_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
+          Variable.variant_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt
     in
       (Globals {h = Free (h, domT --> ranT),
                 y = Free (y, ranT),
diff -r 257e01fab4b7 -r c1f0bc7e7d80 src/HOL/Tools/function_package/mutual.ML
--- a/src/HOL/Tools/function_package/mutual.ML	Sat Sep 30 20:54:34 2006 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML	Sat Sep 30 21:39:17 2006 +0200
@@ -215,7 +215,7 @@
       val thy = ProofContext.theory_of ctxt
 
       val oqnames = map fst pre_qs
-      val (qs, ctxt') = Variable.invent_fixes oqnames ctxt
+      val (qs, ctxt') = Variable.variant_fixes oqnames ctxt
                                            |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
 
       fun inst t = subst_bounds (rev qs, t)
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
diff -r 257e01fab4b7 -r c1f0bc7e7d80 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sat Sep 30 20:54:34 2006 +0200
+++ b/src/Pure/variable.ML	Sat Sep 30 21:39:17 2006 +0200
@@ -33,7 +33,7 @@
   val add_fixes: string list -> Proof.context -> string list * Proof.context
   val add_fixes_direct: string list -> Proof.context -> Proof.context
   val fix_frees: term -> Proof.context -> Proof.context
-  val invent_fixes: string list -> Proof.context -> string list * Proof.context
+  val variant_fixes: string list -> Proof.context -> string list * Proof.context
   val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
   val export_inst: Proof.context -> Proof.context -> string list * string list
   val exportT_inst: Proof.context -> Proof.context -> string list
@@ -199,7 +199,7 @@
 
 val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
 
-fun declare_thm th = fold declare_internal (Thm.full_prop_of th :: Thm.hyps_of th);
+val declare_thm = Drule.fold_terms declare_internal;
 fun thm_context th = declare_thm th (Context.init_proof (Thm.theory_of_thm th));
 
 
@@ -274,7 +274,7 @@
         (xs, fold Name.declare xs names));
   in ctxt |> new_fixes names' xs xs' end;
 
-fun invent_fixes raw_xs ctxt =
+fun variant_fixes raw_xs ctxt =
   let
     val names = names_of ctxt;
     val xs = map Name.clean raw_xs;
@@ -360,7 +360,7 @@
     val ren = if is_open then I else Name.internal;
     val (instT, ctxt') = importT_inst ts ctxt;
     val vars = map (apsnd (TermSubst.instantiateT instT)) (rev (fold Term.add_vars ts []));
-    val (xs, ctxt'') = invent_fixes (map (ren o #1 o #1) vars) ctxt';
+    val (xs, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';
     val inst = vars ~~ map Free (xs ~~ map #2 vars);
   in ((instT, inst), ctxt'') end;
 
@@ -421,7 +421,7 @@
     val t = Thm.term_of goal;
     val ps = Term.variant_frees t (Term.strip_all_vars t);   (*as they are printed :-*)
     val (xs, Ts) = split_list ps;
-    val (xs', ctxt') = invent_fixes xs ctxt;
+    val (xs', ctxt') = variant_fixes xs ctxt;
     val ps' = ListPair.map (cert o Free) (xs', Ts);
     val goal' = fold forall_elim_prop ps' goal;
   in ((ps', goal'), ctxt') end;