# HG changeset patch
# User wenzelm
# Date 1427136183 -3600
# Node ID 6e2a2048689719117456c83382c6bb9ce2cf775c
# Parent  0c73c5eb45f7cd3b036a3af5a3220c56d5322445
local fixes may depend on goal params;

diff -r 0c73c5eb45f7 -r 6e2a20486897 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Mar 23 17:07:43 2015 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Mar 23 19:43:03 2015 +0100
@@ -19,7 +19,7 @@
     val ps = Logic.strip_params (Thm.term_of cgoal);
     val Ts = map snd ps;
     val tinst' = map (fn (t, u) =>
-      (head_of (Logic.incr_indexes (Ts, j) t),
+      (head_of (Logic.incr_indexes ([], Ts, j) t),
        fold_rev Term.abs ps u)) tinst;
     val th' = instf
       (map (apply2 (Thm.ctyp_of ctxt)) tyinst')
diff -r 0c73c5eb45f7 -r 6e2a20486897 src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Mon Mar 23 17:07:43 2015 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Mon Mar 23 19:43:03 2015 +0100
@@ -62,7 +62,7 @@
   let
     val ctxt = Proof_Context.init_global thy
     val maxidx = fold (Term.maxidx_term o Thm.prop_of) intros ~1
-    val pats = map (Logic.incr_indexes ([], maxidx + 1)) pats
+    val pats = map (Logic.incr_indexes ([], [], maxidx + 1)) pats
     val (((pred, intros), pats), ctxt') = import (pred, intros) pats ctxt
     val result_pats = map Var (fold_rev Term.add_vars pats [])
     fun mk_fresh_name names =
diff -r 0c73c5eb45f7 -r 6e2a20486897 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Mar 23 17:07:43 2015 +0100
+++ b/src/Pure/Isar/code.ML	Mon Mar 23 19:43:03 2015 +0100
@@ -1084,7 +1084,7 @@
         val args_of = snd o take_prefix is_Var o rev o snd o strip_comb
           o map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of;
         val args = args_of thm;
-        val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
+        val incr_idx = Logic.incr_indexes ([], [], Thm.maxidx_of thm + 1);
         fun matches_args args' =
           let
             val k = length args' - length args
diff -r 0c73c5eb45f7 -r 6e2a20486897 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Mar 23 17:07:43 2015 +0100
+++ b/src/Pure/Proof/extraction.ML	Mon Mar 23 19:43:03 2015 +0100
@@ -101,7 +101,7 @@
         get_first (fn (_, (prems, (tm1, tm2))) =>
         let
           fun ren t = the_default t (Term.rename_abs tm1 tm t);
-          val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
+          val inc = Logic.incr_indexes ([], [], maxidx_of_term tm + 1);
           val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm) (Vartab.empty, Vartab.empty);
           val prems' = map (apply2 (Envir.subst_term env o inc o ren)) prems;
           val env' = Envir.Envir
diff -r 0c73c5eb45f7 -r 6e2a20486897 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Mon Mar 23 17:07:43 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Mon Mar 23 19:43:03 2015 +0100
@@ -220,8 +220,8 @@
 
     (* local fixes *)
 
-    val fixes_ctxt = param_ctxt
-      |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
+    val (fixed, fixes_ctxt) = param_ctxt
+      |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes;
 
     val (inst_tvars, inst_vars) = read_insts fixes_ctxt mixed_insts thm;
 
@@ -233,7 +233,7 @@
       Var ((a, j + inc), paramTs ---> Logic.incr_tvar inc T);
     fun lift_term t =
       fold_rev Term.absfree (param_names ~~ paramTs)
-        (Logic.incr_indexes (paramTs, inc) t);
+        (Logic.incr_indexes (fixed, paramTs, inc) t);
 
     val inst_tvars' = inst_tvars
       |> map (apply2 (Thm.ctyp_of fixes_ctxt o Logic.incr_tvar inc) o apfst TVar);
diff -r 0c73c5eb45f7 -r 6e2a20486897 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Mon Mar 23 17:07:43 2015 +0100
+++ b/src/Pure/logic.ML	Mon Mar 23 19:43:03 2015 +0100
@@ -61,8 +61,8 @@
   val rlist_abs: (string * typ) list * term -> term
   val incr_tvar_same: int -> typ Same.operation
   val incr_tvar: int -> typ -> typ
-  val incr_indexes_same: typ list * int -> term Same.operation
-  val incr_indexes: typ list * int -> term -> term
+  val incr_indexes_same: string list * typ list * int -> term Same.operation
+  val incr_indexes: string list * typ list * int -> term -> term
   val lift_abs: int -> term -> term -> term
   val lift_all: int -> term -> term -> term
   val strip_assums_hyp: term -> term list
@@ -367,14 +367,18 @@
 
 (*For all variables in the term, increment indexnames and lift over the Us
     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
-fun incr_indexes_same ([], 0) = Same.same
-  | incr_indexes_same (Ts, k) =
+fun incr_indexes_same ([], [], 0) = Same.same
+  | incr_indexes_same (fixed, Ts, k) =
       let
         val n = length Ts;
         val incrT = incr_tvar_same k;
 
         fun incr lev (Var ((x, i), T)) =
               combound (Var ((x, i + k), Ts ---> Same.commit incrT T), lev, n)
+          | incr lev (Free (x, T)) =
+              if member (op =) fixed x then
+                combound (Free (x, Ts ---> Same.commit incrT T), lev, n)
+              else Free (x, incrT T)
           | incr lev (Abs (x, T, body)) =
               (Abs (x, incrT T, incr (lev + 1) body handle Same.SAME => body)
                 handle Same.SAME => Abs (x, T, incr (lev + 1) body))
@@ -382,7 +386,6 @@
               (incr lev t $ (incr lev u handle Same.SAME => u)
                 handle Same.SAME => t $ incr lev u)
           | incr _ (Const (c, T)) = Const (c, incrT T)
-          | incr _ (Free (x, T)) = Free (x, incrT T)
           | incr _ (Bound _) = raise Same.SAME;
       in incr 0 end;
 
@@ -397,14 +400,14 @@
   let
     fun lift Ts (Const ("Pure.imp", _) $ _ $ B) t = lift Ts B t
       | lift Ts (Const ("Pure.all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
-      | lift Ts _ t = incr_indexes (rev Ts, inc) t;
+      | lift Ts _ t = incr_indexes ([], rev Ts, inc) t;
   in lift [] end;
 
 fun lift_all inc =
   let
     fun lift Ts ((c as Const ("Pure.imp", _)) $ A $ B) t = c $ A $ lift Ts B t
       | lift Ts ((c as Const ("Pure.all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
-      | lift Ts _ t = incr_indexes (rev Ts, inc) t;
+      | lift Ts _ t = incr_indexes ([], rev Ts, inc) t;
   in lift [] end;
 
 (*Strips assumptions in goal, yielding list of hypotheses.   *)
diff -r 0c73c5eb45f7 -r 6e2a20486897 src/Pure/more_unify.ML
--- a/src/Pure/more_unify.ML	Mon Mar 23 17:07:43 2015 +0100
+++ b/src/Pure/more_unify.ML	Mon Mar 23 19:43:03 2015 +0100
@@ -28,7 +28,7 @@
 
         val maxidx = fold (Term.maxidx_term o #2) pairs ~1;
         val offset = maxidx + 1;
-        val pairs' = map (apfst (Logic.incr_indexes ([], offset))) pairs;
+        val pairs' = map (apfst (Logic.incr_indexes ([], [], offset))) pairs;
         val maxidx' = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u) pairs' ~1;
 
         val pat_tvars = fold (Term.add_tvars o #1) pairs' [];
diff -r 0c73c5eb45f7 -r 6e2a20486897 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Mar 23 17:07:43 2015 +0100
+++ b/src/Pure/proofterm.ML	Mon Mar 23 19:43:03 2015 +0100
@@ -834,7 +834,7 @@
 fun lift_proof Bi inc prop prf =
   let
     fun lift'' Us Ts t =
-      strip_abs Ts (Logic.incr_indexes (Us, inc) (mk_abs Ts t));
+      strip_abs Ts (Logic.incr_indexes ([], Us, inc) (mk_abs Ts t));
 
     fun lift' Us Ts (Abst (s, T, prf)) =
           (Abst (s, Same.map_option (Logic.incr_tvar_same inc) T, lifth' Us (dummyT::Ts) prf)
@@ -878,7 +878,7 @@
 
 fun incr_indexes i =
   Same.commit (map_proof_terms_same
-    (Logic.incr_indexes_same ([], i)) (Logic.incr_tvar_same i));
+    (Logic.incr_indexes_same ([], [], i)) (Logic.incr_tvar_same i));
 
 
 (***** proof by assumption *****)
diff -r 0c73c5eb45f7 -r 6e2a20486897 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Mar 23 17:07:43 2015 +0100
+++ b/src/Pure/thm.ML	Mon Mar 23 19:43:03 2015 +0100
@@ -278,7 +278,7 @@
 fun incr_indexes_cterm i (ct as Cterm {thy, t, T, maxidx, sorts}) =
   if i < 0 then raise CTERM ("negative increment", [ct])
   else if i = 0 then ct
-  else Cterm {thy = thy, t = Logic.incr_indexes ([], i) t,
+  else Cterm {thy = thy, t = Logic.incr_indexes ([], [], i) t,
     T = Logic.incr_tvar i T, maxidx = maxidx + i, sorts = sorts};
 
 
@@ -1306,8 +1306,8 @@
       maxidx = maxidx + i,
       shyps = shyps,
       hyps = hyps,
-      tpairs = map (apply2 (Logic.incr_indexes ([], i))) tpairs,
-      prop = Logic.incr_indexes ([], i) prop});
+      tpairs = map (apply2 (Logic.incr_indexes ([], [], i))) tpairs,
+      prop = Logic.incr_indexes ([], [], i) prop});
 
 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
 fun assumption opt_ctxt i state =