# HG changeset patch
# User wenzelm
# Date 1230749643 -3600
# Node ID 94b1ffec9201a0407af194c8ef06a68a47a638e4
# Parent  9fa69e3858d6bb1bd663e90ba543df6637bf745d
qualified Term.rename_wrt_term;

diff -r 9fa69e3858d6 -r 94b1ffec9201 src/HOL/Nominal/nominal_inductive.ML
--- 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);
diff -r 9fa69e3858d6 -r 94b1ffec9201 src/HOL/Nominal/nominal_inductive2.ML
--- 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 =
diff -r 9fa69e3858d6 -r 94b1ffec9201 src/HOL/Nominal/nominal_primrec.ML
--- 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
diff -r 9fa69e3858d6 -r 94b1ffec9201 src/HOL/Tools/old_primrec_package.ML
--- 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)))
diff -r 9fa69e3858d6 -r 94b1ffec9201 src/HOL/Tools/primrec_package.ML
--- 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
diff -r 9fa69e3858d6 -r 94b1ffec9201 src/HOL/ex/svc_funcs.ML
--- 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*)
diff -r 9fa69e3858d6 -r 94b1ffec9201 src/Provers/order.ML
--- 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)))
diff -r 9fa69e3858d6 -r 94b1ffec9201 src/Provers/quasi.ML
--- 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)))
diff -r 9fa69e3858d6 -r 94b1ffec9201 src/Pure/Syntax/syn_trans.ML
--- 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 =
diff -r 9fa69e3858d6 -r 94b1ffec9201 src/Pure/logic.ML
--- 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 =
diff -r 9fa69e3858d6 -r 94b1ffec9201 src/Pure/tactic.ML
--- 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);
diff -r 9fa69e3858d6 -r 94b1ffec9201 src/Tools/induct.ML
--- 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): " ^