# HG changeset patch
# User wenzelm
# Date 1121786507 -7200
# Node ID f57b38cced32886985e8ccec044965663e1becee
# Parent  c62bdfbf6a2a3b6a1a5fdc99102b1641d1cd1f0d
Logic.incr_tvar;

diff -r c62bdfbf6a2a -r f57b38cced32 src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Tue Jul 19 17:21:46 2005 +0200
+++ b/src/FOLP/simp.ML	Tue Jul 19 17:21:47 2005 +0200
@@ -593,7 +593,7 @@
 let val sg = sign_of thy;
     val T = case Sign.const_type sg f of
                 NONE => error(f^" not declared") | SOME(T) => T;
-    val T' = incr_tvar 9 T;
+    val T' = Logic.incr_tvar 9 T;
 in mk_cong_type sg (Const(f,T'),T') end;
 
 fun mk_congs thy = List.concat o map (mk_cong_thy thy);
@@ -602,7 +602,7 @@
 let val sg = sign_of thy;
     val S0 = Sign.defaultS sg;
     fun readfT(f,s) =
-        let val T = incr_tvar 9 (Sign.read_typ(sg,K(SOME(S0))) s);
+        let val T = Logic.incr_tvar 9 (Sign.read_typ(sg,K(SOME(S0))) s);
             val t = case Sign.const_type sg f of
                       SOME(_) => Const(f,T) | NONE => Free(f,T)
         in (t,T) end
diff -r c62bdfbf6a2a -r f57b38cced32 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Tue Jul 19 17:21:46 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Tue Jul 19 17:21:47 2005 +0200
@@ -180,7 +180,7 @@
     val tsig = Sign.tsig_of thy;
     val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
     fun varify (t, (i, ts)) =
-      let val t' = map_term_types (incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
+      let val t' = map_term_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
       in (maxidx_of_term t', t'::ts) end;
     val (i, cs') = foldr varify (~1, []) cs;
     val (i', intr_ts') = foldr varify (i, []) intr_ts;
diff -r c62bdfbf6a2a -r f57b38cced32 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Jul 19 17:21:46 2005 +0200
+++ b/src/Pure/Isar/method.ML	Tue Jul 19 17:21:47 2005 +0200
@@ -396,13 +396,13 @@
         val paramTs = map #2 params
         and inc = maxidx+1
         fun liftvar (Var ((a,j), T)) =
-              Var((a, j+inc), paramTs ---> incr_tvar inc T)
+              Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T)
           | liftvar t = raise TERM("Variable expected", [t]);
         fun liftterm t = list_abs_free
               (params, Logic.incr_indexes(paramTs,inc) t)
         fun liftpair (cv,ct) =
               (cterm_fun liftvar cv, cterm_fun liftterm ct)
-        val lifttvar = pairself (ctyp_of sign o incr_tvar inc);
+        val lifttvar = pairself (ctyp_of sign o Logic.incr_tvar inc);
         val rule = Drule.instantiate
               (map lifttvar envT', map liftpair cenv)
               (lift_rule (st, i) thm)
diff -r c62bdfbf6a2a -r f57b38cced32 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Tue Jul 19 17:21:46 2005 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Tue Jul 19 17:21:47 2005 +0200
@@ -75,7 +75,7 @@
       (t as Const (s, T)) = if T = dummyT then (case Sign.const_type sg s of
           NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
         | SOME T => 
-            let val T' = incr_tvar (maxidx + 1) T
+            let val T' = Logic.incr_tvar (maxidx + 1) T
             in (Const (s, T'), T', vTs,
               Envir.Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs})
             end)
@@ -355,7 +355,7 @@
           then (maxidx, prfs, prf) else
           let
             fun inc i =
-              map_proof_terms (Logic.incr_indexes ([], i)) (incr_tvar i);
+              map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i);
             val (maxidx', prf, prfs') =
               (case gen_assoc (op =) (prfs, (a, prop)) of
                 NONE =>
diff -r c62bdfbf6a2a -r f57b38cced32 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Tue Jul 19 17:21:46 2005 +0200
+++ b/src/Pure/tactic.ML	Tue Jul 19 17:21:47 2005 +0200
@@ -256,13 +256,13 @@
     and params = params_of_state st i
     val paramTs = map #2 params
     and inc = maxidx+1
-    fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> incr_tvar inc T)
+    fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
       | liftvar t = raise TERM("Variable expected", [t]);
     fun liftterm t = list_abs_free (params,
                                     Logic.incr_indexes(paramTs,inc) t)
     (*Lifts instantiation pair over params*)
     fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
-    val lifttvar = pairself (ctyp_fun (incr_tvar inc))
+    val lifttvar = pairself (ctyp_fun (Logic.incr_tvar inc))
 in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
                      (lift_rule (st,i) rule)
 end;
@@ -289,12 +289,12 @@
 let val {maxidx,thy,...} = rep_thm st
     val paramTs = map #2 (params_of_state st i)
     and inc = maxidx+1
-    fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> incr_tvar inc T)
+    fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
     (*lift only Var, not term, which must be lifted already*)
     fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t)
     fun liftTpair (((a, i), S), T) =
       (ctyp_of thy (TVar ((a, i + inc), S)),
-       ctyp_of thy (incr_tvar inc T))
+       ctyp_of thy (Logic.incr_tvar inc T))
 in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
                      (lift_rule (st,i) rule)
 end;