--- 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
--- 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.
--- 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),
--- 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)
--- 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
--- 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;