--- a/src/HOL/Nominal/nominal_inductive.ML Wed Dec 31 18:53:19 2008 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Wed Dec 31 19:54:03 2008 +0100
@@ -240,7 +240,7 @@
if null (OldTerm.term_frees prem inter ps) then prem
else lift_prem prem) prems,
HOLogic.mk_Trueprop (lift_pred p ts));
- val vs = map (Var o apfst (rpair 0)) (rename_wrt_term prem params')
+ val vs = map (Var o apfst (rpair 0)) (Term.rename_wrt_term prem params')
in
(list_all (params', prem), (rev vs, subst_bounds (vs, prem)))
end) prems);
--- a/src/HOL/Nominal/nominal_inductive2.ML Wed Dec 31 18:53:19 2008 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML Wed Dec 31 19:54:03 2008 +0100
@@ -138,7 +138,7 @@
in Option.map prove (map_term f prop (the_default prop opt)) end;
fun abs_params params t =
- let val vs = map (Var o apfst (rpair 0)) (rename_wrt_term t params)
+ let val vs = map (Var o apfst (rpair 0)) (Term.rename_wrt_term t params)
in (list_all (params, t), (rev vs, subst_bounds (vs, t))) end;
fun inst_params thy (vs, p) th cts =
--- a/src/HOL/Nominal/nominal_primrec.ML Wed Dec 31 18:53:19 2008 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Wed Dec 31 19:54:03 2008 +0100
@@ -155,7 +155,7 @@
val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
val rargs = map fst recs;
val subs = map (rpair dummyT o fst)
- (rev (rename_wrt_term rhs rargs));
+ (rev (Term.rename_wrt_term rhs rargs));
val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
(Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
handle RecError s => primrec_eq_err lthy s eq
--- a/src/HOL/Tools/old_primrec_package.ML Wed Dec 31 18:53:19 2008 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML Wed Dec 31 19:54:03 2008 +0100
@@ -161,7 +161,7 @@
val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
val rargs = map fst recs;
val subs = map (rpair dummyT o fst)
- (rev (rename_wrt_term rhs rargs));
+ (rev (Term.rename_wrt_term rhs rargs));
val (rhs', (fnameTs'', fnss'')) =
(subst (map (fn ((x, y), z) =>
(Free x, (body_index y, Free z)))
--- a/src/HOL/Tools/primrec_package.ML Wed Dec 31 18:53:19 2008 +0100
+++ b/src/HOL/Tools/primrec_package.ML Wed Dec 31 19:54:03 2008 +0100
@@ -141,7 +141,7 @@
val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
val rargs = map fst recs;
val subs = map (rpair dummyT o fst)
- (rev (rename_wrt_term rhs rargs));
+ (rev (Term.rename_wrt_term rhs rargs));
val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
(Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
handle PrimrecError (s, NONE) => primrec_error_eqn s eq
--- a/src/HOL/ex/svc_funcs.ML Wed Dec 31 18:53:19 2008 +0100
+++ b/src/HOL/ex/svc_funcs.ML Wed Dec 31 19:54:03 2008 +0100
@@ -1,9 +1,8 @@
(* Title: HOL/ex/svc_funcs.ML
- ID: $Id$
Author: Lawrence C Paulson
Copyright 1999 University of Cambridge
-Translation functions for the interface to SVC
+Translation functions for the interface to SVC.
Based upon the work of Soren T. Heilmann
@@ -126,7 +125,7 @@
pos ["positive"]: true if an assumption, false if a goal*)
fun expr_of pos t =
let
- val params = rev (rename_wrt_term t (Term.strip_all_vars t))
+ val params = rev (Term.rename_wrt_term t (Term.strip_all_vars t))
and body = Term.strip_all_body t
val nat_vars = ref ([] : string list)
(*translation of a variable: record all natural numbers*)
--- a/src/Provers/order.ML Wed Dec 31 18:53:19 2008 +0100
+++ b/src/Provers/order.ML Wed Dec 31 19:54:03 2008 +0100
@@ -1,8 +1,6 @@
-(*
- Title: Transitivity reasoner for partial and linear orders
- Id: $Id$
- Author: Oliver Kutter
- Copyright: TU Muenchen
+(* Author: Oliver Kutter, TU Muenchen
+
+Transitivity reasoner for partial and linear orders.
*)
(* TODO: reduce number of input thms *)
@@ -1234,7 +1232,7 @@
SUBGOAL (fn (A, n, sign) =>
let
- val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
+ val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A))
val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
val lesss = List.concat (ListPair.map (mkasm decomp less_thms sign) (Hs, 0 upto (length Hs - 1)))
--- a/src/Provers/quasi.ML Wed Dec 31 18:53:19 2008 +0100
+++ b/src/Provers/quasi.ML Wed Dec 31 19:54:03 2008 +0100
@@ -1,9 +1,7 @@
-(*
- Title: Reasoner for simple transitivity and quasi orders.
- Id: $Id$
- Author: Oliver Kutter
- Copyright: TU Muenchen
- *)
+(* Author: Oliver Kutter, TU Muenchen
+
+Reasoner for simple transitivity and quasi orders.
+*)
(*
@@ -557,7 +555,7 @@
(* trans_tac - solves transitivity chains over <= *)
val trans_tac = SUBGOAL (fn (A, n, sign) =>
let
- val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
+ val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A))
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
val lesss = List.concat (ListPair.map (mkasm_trans sign) (Hs, 0 upto (length Hs - 1)))
@@ -578,7 +576,7 @@
(* quasi_tac - solves quasi orders *)
val quasi_tac = SUBGOAL (fn (A, n, sign) =>
let
- val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
+ val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A))
val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
val lesss = List.concat (ListPair.map (mkasm_quasi sign) (Hs, 0 upto (length Hs - 1)))
--- a/src/Pure/Syntax/syn_trans.ML Wed Dec 31 18:53:19 2008 +0100
+++ b/src/Pure/Syntax/syn_trans.ML Wed Dec 31 19:54:03 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Syntax/syn_trans.ML
- ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
Syntax translation functions.
@@ -264,7 +263,7 @@
let
val vars = vars_of tm;
val body = body_of tm;
- val rev_new_vars = rename_wrt_term body vars;
+ val rev_new_vars = Term.rename_wrt_term body vars;
fun subst (x, T) b =
if can Name.dest_internal x andalso not (Term.loose_bvar1 (b, 0))
then (Const ("_idtdummy", T), incr_boundvars ~1 b)
@@ -302,7 +301,7 @@
(strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
fun atomic_abs_tr' (x, T, t) =
- let val [xT] = rename_wrt_term t [(x, T)]
+ let val [xT] = Term.rename_wrt_term t [(x, T)]
in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end;
fun abs_ast_tr' (*"_abs"*) asts =
--- a/src/Pure/logic.ML Wed Dec 31 18:53:19 2008 +0100
+++ b/src/Pure/logic.ML Wed Dec 31 19:54:03 2008 +0100
@@ -1,7 +1,6 @@
(* Title: Pure/logic.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright Cambridge University 1992
+ Author: Makarius
Abstract syntax operations of the Pure meta-logic.
*)
@@ -515,7 +514,7 @@
(*reverses parameters for substitution*)
fun goal_params st i =
let val gi = get_goal st i
- val rfrees = map Free (rename_wrt_term gi (strip_params gi))
+ val rfrees = map Free (Term.rename_wrt_term gi (strip_params gi))
in (gi, rfrees) end;
fun concl_of_goal st i =
--- a/src/Pure/tactic.ML Wed Dec 31 18:53:19 2008 +0100
+++ b/src/Pure/tactic.ML Wed Dec 31 19:54:03 2008 +0100
@@ -1,9 +1,7 @@
(* Title: Pure/tactic.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1991 University of Cambridge
-Basic tactics.
+Fundamental tactics.
*)
signature BASIC_TACTIC =
@@ -192,7 +190,7 @@
(*Determine print names of goal parameters (reversed)*)
fun innermost_params i st =
let val (_, _, Bi, _) = dest_state (st, i)
- in rename_wrt_term Bi (Logic.strip_params Bi) end;
+ in Term.rename_wrt_term Bi (Logic.strip_params Bi) end;
(*params of subgoal i as they are printed*)
fun params_of_state i st = rev (innermost_params i st);
--- a/src/Tools/induct.ML Wed Dec 31 18:53:19 2008 +0100
+++ b/src/Tools/induct.ML Wed Dec 31 19:54:03 2008 +0100
@@ -440,7 +440,7 @@
val thy = ProofContext.theory_of ctxt;
val maxidx = Thm.maxidx_of st;
val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*)
- val params = rev (rename_wrt_term goal (Logic.strip_params goal));
+ val params = rev (Term.rename_wrt_term goal (Logic.strip_params goal));
in
if not (null params) then
(warning ("Cannot determine rule instantiation due to pending parameter(s): " ^