Thm.adjust_maxidx;

--- a/src/Pure/axclass.ML	Sun Jul 30 21:28:51 2006 +0200
+++ b/src/Pure/axclass.ML	Sun Jul 30 21:28:52 2006 +0200
@@ -425,7 +425,7 @@
       sort |> map (fn c =>
         Goal.finish (the (lookup_type cache' typ c) RS
           Goal.init (Thm.cterm_of thy (Logic.mk_inclass (typ, c))))
-        |> Thm.adjust_maxidx_thm);
+        |> Thm.adjust_maxidx_thm ~1);
   in (ths, cache') end;
 
 end;

--- a/src/Pure/conjunction.ML	Sun Jul 30 21:28:51 2006 +0200
+++ b/src/Pure/conjunction.ML	Sun Jul 30 21:28:52 2006 +0200
@@ -139,7 +139,7 @@
 val B = Free ("B", propT);
 
 fun comp_rule th rule =
-  Thm.adjust_maxidx_thm (th COMP
+  Thm.adjust_maxidx_thm ~1 (th COMP
     (rule |> Drule.forall_intr_frees |> Drule.forall_elim_vars (Thm.maxidx_of th + 1)));
 
 in

--- a/src/Pure/drule.ML	Sun Jul 30 21:28:51 2006 +0200
+++ b/src/Pure/drule.ML	Sun Jul 30 21:28:52 2006 +0200
@@ -416,7 +416,7 @@
     val (instT, inst) = Term.zero_var_indexes_inst (Thm.full_prop_of th);
     val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT;
     val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst;
-  in Thm.adjust_maxidx_thm (Thm.instantiate (cinstT, cinst) th) end;
+  in Thm.adjust_maxidx_thm ~1 (Thm.instantiate (cinstT, cinst) th) end;
 
 
 (** Standard form of object-rule: no hypotheses, flexflex constraints,

--- a/src/Pure/goal.ML	Sun Jul 30 21:28:51 2006 +0200
+++ b/src/Pure/goal.ML	Sun Jul 30 21:28:52 2006 +0200
@@ -153,7 +153,7 @@
   (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
    else if n = 1 then Seq.single (Thm.cprem_of st i)
    else Seq.single (foldr1 Conjunction.mk_conjunction (map (Thm.cprem_of st) (i upto i + n - 1))))
-  |> Seq.map (Thm.adjust_maxidx #> init);
+  |> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init);
 
 fun retrofit i n st' st =
   (if n = 1 then st

--- a/src/Pure/meta_simplifier.ML	Sun Jul 30 21:28:51 2006 +0200
+++ b/src/Pure/meta_simplifier.ML	Sun Jul 30 21:28:52 2006 +0200
@@ -1161,7 +1161,7 @@
 
 fun rewrite_cterm mode prover raw_ss raw_ct =
   let
-    val ct = Thm.adjust_maxidx raw_ct;
+    val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
     val {thy, t, maxidx, ...} = Thm.rep_cterm ct;
     val ss = fallback_context thy raw_ss;
     val _ = inc simp_depth;
@@ -1210,7 +1210,7 @@
 fun gen_norm_hhf ss =
   (not o Drule.is_norm_hhf o Thm.prop_of) ?
     Drule.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) ss)
-  #> Thm.adjust_maxidx_thm
+  #> Thm.adjust_maxidx_thm ~1
   #> Drule.gen_all;
 
 val ss = theory_context ProtoPure.thy empty_ss addsimps [Drule.norm_hhf_eq];