qualified Term.rename_wrt_term;
authorwenzelm
Wed Dec 31 19:54:03 2008 +0100 (2008-12-31)
changeset 2927694b1ffec9201
parent 29275 9fa69e3858d6
child 29277 29dd1c516337
qualified Term.rename_wrt_term;
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/old_primrec_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/ex/svc_funcs.ML
src/Provers/order.ML
src/Provers/quasi.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/logic.ML
src/Pure/tactic.ML
src/Tools/induct.ML
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Wed Dec 31 18:53:19 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Dec 31 19:54:03 2008 +0100
     1.3 @@ -240,7 +240,7 @@
     1.4               if null (OldTerm.term_frees prem inter ps) then prem
     1.5               else lift_prem prem) prems,
     1.6             HOLogic.mk_Trueprop (lift_pred p ts));
     1.7 -        val vs = map (Var o apfst (rpair 0)) (rename_wrt_term prem params')
     1.8 +        val vs = map (Var o apfst (rpair 0)) (Term.rename_wrt_term prem params')
     1.9        in
    1.10          (list_all (params', prem), (rev vs, subst_bounds (vs, prem)))
    1.11        end) prems);
     2.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Dec 31 18:53:19 2008 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Dec 31 19:54:03 2008 +0100
     2.3 @@ -138,7 +138,7 @@
     2.4    in Option.map prove (map_term f prop (the_default prop opt)) end;
     2.5  
     2.6  fun abs_params params t =
     2.7 -  let val vs =  map (Var o apfst (rpair 0)) (rename_wrt_term t params)
     2.8 +  let val vs =  map (Var o apfst (rpair 0)) (Term.rename_wrt_term t params)
     2.9    in (list_all (params, t), (rev vs, subst_bounds (vs, t))) end;
    2.10  
    2.11  fun inst_params thy (vs, p) th cts =
     3.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Wed Dec 31 18:53:19 2008 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Dec 31 19:54:03 2008 +0100
     3.3 @@ -155,7 +155,7 @@
     3.4                val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
     3.5                val rargs = map fst recs;
     3.6                val subs = map (rpair dummyT o fst)
     3.7 -                (rev (rename_wrt_term rhs rargs));
     3.8 +                (rev (Term.rename_wrt_term rhs rargs));
     3.9                val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
    3.10                  (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
    3.11                    handle RecError s => primrec_eq_err lthy s eq
     4.1 --- a/src/HOL/Tools/old_primrec_package.ML	Wed Dec 31 18:53:19 2008 +0100
     4.2 +++ b/src/HOL/Tools/old_primrec_package.ML	Wed Dec 31 19:54:03 2008 +0100
     4.3 @@ -161,7 +161,7 @@
     4.4                val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
     4.5                val rargs = map fst recs;
     4.6                val subs = map (rpair dummyT o fst)
     4.7 -                (rev (rename_wrt_term rhs rargs));
     4.8 +                (rev (Term.rename_wrt_term rhs rargs));
     4.9                val (rhs', (fnameTs'', fnss'')) =
    4.10                    (subst (map (fn ((x, y), z) =>
    4.11                                 (Free x, (body_index y, Free z)))
     5.1 --- a/src/HOL/Tools/primrec_package.ML	Wed Dec 31 18:53:19 2008 +0100
     5.2 +++ b/src/HOL/Tools/primrec_package.ML	Wed Dec 31 19:54:03 2008 +0100
     5.3 @@ -141,7 +141,7 @@
     5.4                val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
     5.5                val rargs = map fst recs;
     5.6                val subs = map (rpair dummyT o fst)
     5.7 -                (rev (rename_wrt_term rhs rargs));
     5.8 +                (rev (Term.rename_wrt_term rhs rargs));
     5.9                val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
    5.10                  (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
    5.11                    handle PrimrecError (s, NONE) => primrec_error_eqn s eq
     6.1 --- a/src/HOL/ex/svc_funcs.ML	Wed Dec 31 18:53:19 2008 +0100
     6.2 +++ b/src/HOL/ex/svc_funcs.ML	Wed Dec 31 19:54:03 2008 +0100
     6.3 @@ -1,9 +1,8 @@
     6.4  (*  Title:      HOL/ex/svc_funcs.ML
     6.5 -    ID:         $Id$
     6.6      Author:     Lawrence C Paulson
     6.7      Copyright   1999  University of Cambridge
     6.8  
     6.9 -Translation functions for the interface to SVC
    6.10 +Translation functions for the interface to SVC.
    6.11  
    6.12  Based upon the work of Soren T. Heilmann
    6.13  
    6.14 @@ -126,7 +125,7 @@
    6.15     pos ["positive"]: true if an assumption, false if a goal*)
    6.16   fun expr_of pos t =
    6.17    let
    6.18 -    val params = rev (rename_wrt_term t (Term.strip_all_vars t))
    6.19 +    val params = rev (Term.rename_wrt_term t (Term.strip_all_vars t))
    6.20      and body   = Term.strip_all_body t
    6.21      val nat_vars = ref ([] : string list)
    6.22      (*translation of a variable: record all natural numbers*)
     7.1 --- a/src/Provers/order.ML	Wed Dec 31 18:53:19 2008 +0100
     7.2 +++ b/src/Provers/order.ML	Wed Dec 31 19:54:03 2008 +0100
     7.3 @@ -1,8 +1,6 @@
     7.4 -(*
     7.5 -  Title:	Transitivity reasoner for partial and linear orders
     7.6 -  Id:		$Id$
     7.7 -  Author:	Oliver Kutter
     7.8 -  Copyright:	TU Muenchen
     7.9 +(*  Author:     Oliver Kutter, TU Muenchen
    7.10 +
    7.11 +Transitivity reasoner for partial and linear orders.
    7.12  *)
    7.13  
    7.14  (* TODO: reduce number of input thms *)
    7.15 @@ -1234,7 +1232,7 @@
    7.16  
    7.17      SUBGOAL (fn (A, n, sign) =>
    7.18       let
    7.19 -      val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
    7.20 +      val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A))
    7.21        val Hs = map prop_of prems @ map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
    7.22        val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
    7.23        val lesss = List.concat (ListPair.map (mkasm decomp less_thms sign) (Hs, 0 upto (length Hs - 1)))
     8.1 --- a/src/Provers/quasi.ML	Wed Dec 31 18:53:19 2008 +0100
     8.2 +++ b/src/Provers/quasi.ML	Wed Dec 31 19:54:03 2008 +0100
     8.3 @@ -1,9 +1,7 @@
     8.4 -(* 
     8.5 -   Title:	Reasoner for simple transitivity and quasi orders. 
     8.6 -   Id:		$Id$
     8.7 -   Author:	Oliver Kutter
     8.8 -   Copyright:	TU Muenchen
     8.9 - *)
    8.10 +(*  Author:     Oliver Kutter, TU Muenchen
    8.11 +
    8.12 +Reasoner for simple transitivity and quasi orders.
    8.13 +*)
    8.14  
    8.15  (* 
    8.16   
    8.17 @@ -557,7 +555,7 @@
    8.18  (* trans_tac - solves transitivity chains over <= *)
    8.19  val trans_tac  =  SUBGOAL (fn (A, n, sign) =>
    8.20   let
    8.21 -  val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
    8.22 +  val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A))
    8.23    val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
    8.24    val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
    8.25    val lesss = List.concat (ListPair.map (mkasm_trans  sign) (Hs, 0 upto (length Hs - 1)))
    8.26 @@ -578,7 +576,7 @@
    8.27  (* quasi_tac - solves quasi orders *)
    8.28  val quasi_tac = SUBGOAL (fn (A, n, sign) =>
    8.29   let
    8.30 -  val rfrees = map Free (rename_wrt_term A (Logic.strip_params A))
    8.31 +  val rfrees = map Free (Term.rename_wrt_term A (Logic.strip_params A))
    8.32    val Hs = map (fn H => subst_bounds (rfrees, H)) (Logic.strip_assums_hyp A)
    8.33    val C = subst_bounds (rfrees, Logic.strip_assums_concl A)
    8.34    val lesss = List.concat (ListPair.map (mkasm_quasi sign) (Hs, 0 upto (length Hs - 1)))
     9.1 --- a/src/Pure/Syntax/syn_trans.ML	Wed Dec 31 18:53:19 2008 +0100
     9.2 +++ b/src/Pure/Syntax/syn_trans.ML	Wed Dec 31 19:54:03 2008 +0100
     9.3 @@ -1,5 +1,4 @@
     9.4  (*  Title:      Pure/Syntax/syn_trans.ML
     9.5 -    ID:         $Id$
     9.6      Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     9.7  
     9.8  Syntax translation functions.
     9.9 @@ -264,7 +263,7 @@
    9.10    let
    9.11      val vars = vars_of tm;
    9.12      val body = body_of tm;
    9.13 -    val rev_new_vars = rename_wrt_term body vars;
    9.14 +    val rev_new_vars = Term.rename_wrt_term body vars;
    9.15      fun subst (x, T) b =
    9.16        if can Name.dest_internal x andalso not (Term.loose_bvar1 (b, 0))
    9.17        then (Const ("_idtdummy", T), incr_boundvars ~1 b)
    9.18 @@ -302,7 +301,7 @@
    9.19      (strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
    9.20  
    9.21  fun atomic_abs_tr' (x, T, t) =
    9.22 -  let val [xT] = rename_wrt_term t [(x, T)]
    9.23 +  let val [xT] = Term.rename_wrt_term t [(x, T)]
    9.24    in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end;
    9.25  
    9.26  fun abs_ast_tr' (*"_abs"*) asts =
    10.1 --- a/src/Pure/logic.ML	Wed Dec 31 18:53:19 2008 +0100
    10.2 +++ b/src/Pure/logic.ML	Wed Dec 31 19:54:03 2008 +0100
    10.3 @@ -1,7 +1,6 @@
    10.4  (*  Title:      Pure/logic.ML
    10.5 -    ID:         $Id$
    10.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.7 -    Copyright   Cambridge University 1992
    10.8 +    Author:     Makarius
    10.9  
   10.10  Abstract syntax operations of the Pure meta-logic.
   10.11  *)
   10.12 @@ -515,7 +514,7 @@
   10.13  (*reverses parameters for substitution*)
   10.14  fun goal_params st i =
   10.15    let val gi = get_goal st i
   10.16 -      val rfrees = map Free (rename_wrt_term gi (strip_params gi))
   10.17 +      val rfrees = map Free (Term.rename_wrt_term gi (strip_params gi))
   10.18    in (gi, rfrees) end;
   10.19  
   10.20  fun concl_of_goal st i =
    11.1 --- a/src/Pure/tactic.ML	Wed Dec 31 18:53:19 2008 +0100
    11.2 +++ b/src/Pure/tactic.ML	Wed Dec 31 19:54:03 2008 +0100
    11.3 @@ -1,9 +1,7 @@
    11.4  (*  Title:      Pure/tactic.ML
    11.5 -    ID:         $Id$
    11.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.7 -    Copyright   1991  University of Cambridge
    11.8  
    11.9 -Basic tactics.
   11.10 +Fundamental tactics.
   11.11  *)
   11.12  
   11.13  signature BASIC_TACTIC =
   11.14 @@ -192,7 +190,7 @@
   11.15  (*Determine print names of goal parameters (reversed)*)
   11.16  fun innermost_params i st =
   11.17    let val (_, _, Bi, _) = dest_state (st, i)
   11.18 -  in rename_wrt_term Bi (Logic.strip_params Bi) end;
   11.19 +  in Term.rename_wrt_term Bi (Logic.strip_params Bi) end;
   11.20  
   11.21  (*params of subgoal i as they are printed*)
   11.22  fun params_of_state i st = rev (innermost_params i st);
    12.1 --- a/src/Tools/induct.ML	Wed Dec 31 18:53:19 2008 +0100
    12.2 +++ b/src/Tools/induct.ML	Wed Dec 31 19:54:03 2008 +0100
    12.3 @@ -440,7 +440,7 @@
    12.4      val thy = ProofContext.theory_of ctxt;
    12.5      val maxidx = Thm.maxidx_of st;
    12.6      val goal = Thm.term_of (Thm.cprem_of st i);  (*exception Subscript*)
    12.7 -    val params = rev (rename_wrt_term goal (Logic.strip_params goal));
    12.8 +    val params = rev (Term.rename_wrt_term goal (Logic.strip_params goal));
    12.9    in
   12.10      if not (null params) then
   12.11        (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^