Logic.incr_tvar;
authorwenzelm
Tue Jul 19 17:21:47 2005 +0200 (2005-07-19)
changeset 16876f57b38cced32
parent 16875 c62bdfbf6a2a
child 16877 e92cba1d4842
Logic.incr_tvar;
src/FOLP/simp.ML
src/HOL/Tools/inductive_package.ML
src/Pure/Isar/method.ML
src/Pure/Proof/reconstruct.ML
src/Pure/tactic.ML
     1.1 --- a/src/FOLP/simp.ML	Tue Jul 19 17:21:46 2005 +0200
     1.2 +++ b/src/FOLP/simp.ML	Tue Jul 19 17:21:47 2005 +0200
     1.3 @@ -593,7 +593,7 @@
     1.4  let val sg = sign_of thy;
     1.5      val T = case Sign.const_type sg f of
     1.6                  NONE => error(f^" not declared") | SOME(T) => T;
     1.7 -    val T' = incr_tvar 9 T;
     1.8 +    val T' = Logic.incr_tvar 9 T;
     1.9  in mk_cong_type sg (Const(f,T'),T') end;
    1.10  
    1.11  fun mk_congs thy = List.concat o map (mk_cong_thy thy);
    1.12 @@ -602,7 +602,7 @@
    1.13  let val sg = sign_of thy;
    1.14      val S0 = Sign.defaultS sg;
    1.15      fun readfT(f,s) =
    1.16 -        let val T = incr_tvar 9 (Sign.read_typ(sg,K(SOME(S0))) s);
    1.17 +        let val T = Logic.incr_tvar 9 (Sign.read_typ(sg,K(SOME(S0))) s);
    1.18              val t = case Sign.const_type sg f of
    1.19                        SOME(_) => Const(f,T) | NONE => Free(f,T)
    1.20          in (t,T) end
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Jul 19 17:21:46 2005 +0200
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Jul 19 17:21:47 2005 +0200
     2.3 @@ -180,7 +180,7 @@
     2.4      val tsig = Sign.tsig_of thy;
     2.5      val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
     2.6      fun varify (t, (i, ts)) =
     2.7 -      let val t' = map_term_types (incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
     2.8 +      let val t' = map_term_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
     2.9        in (maxidx_of_term t', t'::ts) end;
    2.10      val (i, cs') = foldr varify (~1, []) cs;
    2.11      val (i', intr_ts') = foldr varify (i, []) intr_ts;
     3.1 --- a/src/Pure/Isar/method.ML	Tue Jul 19 17:21:46 2005 +0200
     3.2 +++ b/src/Pure/Isar/method.ML	Tue Jul 19 17:21:47 2005 +0200
     3.3 @@ -396,13 +396,13 @@
     3.4          val paramTs = map #2 params
     3.5          and inc = maxidx+1
     3.6          fun liftvar (Var ((a,j), T)) =
     3.7 -              Var((a, j+inc), paramTs ---> incr_tvar inc T)
     3.8 +              Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T)
     3.9            | liftvar t = raise TERM("Variable expected", [t]);
    3.10          fun liftterm t = list_abs_free
    3.11                (params, Logic.incr_indexes(paramTs,inc) t)
    3.12          fun liftpair (cv,ct) =
    3.13                (cterm_fun liftvar cv, cterm_fun liftterm ct)
    3.14 -        val lifttvar = pairself (ctyp_of sign o incr_tvar inc);
    3.15 +        val lifttvar = pairself (ctyp_of sign o Logic.incr_tvar inc);
    3.16          val rule = Drule.instantiate
    3.17                (map lifttvar envT', map liftpair cenv)
    3.18                (lift_rule (st, i) thm)
     4.1 --- a/src/Pure/Proof/reconstruct.ML	Tue Jul 19 17:21:46 2005 +0200
     4.2 +++ b/src/Pure/Proof/reconstruct.ML	Tue Jul 19 17:21:47 2005 +0200
     4.3 @@ -75,7 +75,7 @@
     4.4        (t as Const (s, T)) = if T = dummyT then (case Sign.const_type sg s of
     4.5            NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
     4.6          | SOME T => 
     4.7 -            let val T' = incr_tvar (maxidx + 1) T
     4.8 +            let val T' = Logic.incr_tvar (maxidx + 1) T
     4.9              in (Const (s, T'), T', vTs,
    4.10                Envir.Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs})
    4.11              end)
    4.12 @@ -355,7 +355,7 @@
    4.13            then (maxidx, prfs, prf) else
    4.14            let
    4.15              fun inc i =
    4.16 -              map_proof_terms (Logic.incr_indexes ([], i)) (incr_tvar i);
    4.17 +              map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i);
    4.18              val (maxidx', prf, prfs') =
    4.19                (case gen_assoc (op =) (prfs, (a, prop)) of
    4.20                  NONE =>
     5.1 --- a/src/Pure/tactic.ML	Tue Jul 19 17:21:46 2005 +0200
     5.2 +++ b/src/Pure/tactic.ML	Tue Jul 19 17:21:47 2005 +0200
     5.3 @@ -256,13 +256,13 @@
     5.4      and params = params_of_state st i
     5.5      val paramTs = map #2 params
     5.6      and inc = maxidx+1
     5.7 -    fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T)
     5.8 +    fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
     5.9        | liftvar t = raise TERM("Variable expected", [t]);
    5.10      fun liftterm t = list_abs_free (params,
    5.11                                      Logic.incr_indexes(paramTs,inc) t)
    5.12      (*Lifts instantiation pair over params*)
    5.13      fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
    5.14 -    val lifttvar = pairself (ctyp_fun (incr_tvar inc))
    5.15 +    val lifttvar = pairself (ctyp_fun (Logic.incr_tvar inc))
    5.16  in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
    5.17                       (lift_rule (st,i) rule)
    5.18  end;
    5.19 @@ -289,12 +289,12 @@
    5.20  let val {maxidx,thy,...} = rep_thm st
    5.21      val paramTs = map #2 (params_of_state st i)
    5.22      and inc = maxidx+1
    5.23 -    fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> incr_tvar inc T)
    5.24 +    fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
    5.25      (*lift only Var, not term, which must be lifted already*)
    5.26      fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t)
    5.27      fun liftTpair (((a, i), S), T) =
    5.28        (ctyp_of thy (TVar ((a, i + inc), S)),
    5.29 -       ctyp_of thy (incr_tvar inc T))
    5.30 +       ctyp_of thy (Logic.incr_tvar inc T))
    5.31  in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
    5.32                       (lift_rule (st,i) rule)
    5.33  end;