1.1 --- a/src/Pure/thm.ML	Tue Aug 09 22:37:33 2011 +0200
     1.2 +++ b/src/Pure/thm.ML	Tue Aug 09 23:54:17 2011 +0200
     1.3 @@ -1515,44 +1515,61 @@
     1.4         prop = prop'}));
     1.5  
     1.6  
     1.7 -(* strip_apply f (A, B) strips off all assumptions/parameters from A
     1.8 +(* strip_apply f B A strips off all assumptions/parameters from A
     1.9     introduced by lifting over B, and applies f to remaining part of A*)
    1.10  fun strip_apply f =
    1.11 -  let fun strip(Const("==>",_)$ A1 $ B1,
    1.12 -                Const("==>",_)$ _  $ B2) = Logic.mk_implies (A1, strip(B1,B2))
    1.13 -        | strip((c as Const("all",_)) $ Abs(a,T,t1),
    1.14 -                      Const("all",_)  $ Abs(_,_,t2)) = c$Abs(a,T,strip(t1,t2))
    1.15 -        | strip(A,_) = f A
    1.16 +  let fun strip (Const ("==>", _) $ _  $ B1)
    1.17 +                (Const ("==>", _) $ A2 $ B2) = Logic.mk_implies (A2, strip B1 B2)
    1.18 +        | strip ((c as Const ("all", _)) $ Abs (_, _, t1))
    1.19 +                (      Const ("all", _)  $ Abs (a, T, t2)) = c $ Abs (a, T, strip t1 t2)
    1.20 +        | strip _ A = f A
    1.21    in strip end;
    1.22  
    1.23 +fun strip_lifted (Const ("==>", _) $ _ $ B1)
    1.24 +                 (Const ("==>", _) $ _ $ B2) = strip_lifted B1 B2
    1.25 +  | strip_lifted (Const ("all", _) $ Abs (_, _, t1))
    1.26 +                 (Const ("all", _) $ Abs (_, _, t2)) = strip_lifted t1 t2
    1.27 +  | strip_lifted _ A = A;
    1.28 +
    1.29  (*Use the alist to rename all bound variables and some unknowns in a term
    1.30    dpairs = current disagreement pairs;  tpairs = permanent ones (flexflex);
    1.31    Preserves unknowns in tpairs and on lhs of dpairs. *)
    1.32 -fun rename_bvs([],_,_,_) = I
    1.33 -  | rename_bvs(al,dpairs,tpairs,B) =
    1.34 +fun rename_bvs [] _ _ _ _ = K I
    1.35 +  | rename_bvs al dpairs tpairs B As =
    1.36        let
    1.37          val add_var = fold_aterms (fn Var ((x, _), _) => insert (op =) x | _ => I);
    1.38          val vids = []
    1.39            |> fold (add_var o fst) dpairs
    1.40            |> fold (add_var o fst) tpairs
    1.41            |> fold (add_var o snd) tpairs;
    1.42 +        val vids' = fold (add_var o strip_lifted B) As [];
    1.43          (*unknowns appearing elsewhere be preserved!*)
    1.44 -        fun rename(t as Var((x,i),T)) =
    1.45 -              (case AList.lookup (op =) al x of
    1.46 -                SOME y =>
    1.47 -                  if member (op =) vids x orelse member (op =) vids y then t
    1.48 -                  else Var((y,i),T)
    1.49 -              | NONE=> t)
    1.50 -          | rename(Abs(x,T,t)) =
    1.51 +        val al' = distinct ((op =) o pairself fst)
    1.52 +          (filter_out (fn (x, y) =>
    1.53 +             not (member (op =) vids' x) orelse
    1.54 +             member (op =) vids x orelse member (op =) vids y) al);
    1.55 +        val unchanged = filter_out (AList.defined (op =) al') vids';
    1.56 +        fun del_clashing clash xs _ [] qs =
    1.57 +              if clash then del_clashing false xs xs qs [] else qs
    1.58 +          | del_clashing clash xs ys ((p as (x, y)) :: ps) qs =
    1.59 +              if member (op =) ys y
    1.60 +              then del_clashing true (x :: xs) (x :: ys) ps qs
    1.61 +              else del_clashing clash xs (y :: ys) ps (p :: qs);
    1.62 +        val al'' = del_clashing false unchanged unchanged al' [];        
    1.63 +        fun rename (t as Var ((x, i), T)) =
    1.64 +              (case AList.lookup (op =) al'' x of
    1.65 +                 SOME y => Var ((y, i), T)
    1.66 +               | NONE => t)
    1.67 +          | rename (Abs (x, T, t)) =
    1.68                Abs (the_default x (AList.lookup (op =) al x), T, rename t)
    1.69 -          | rename(f$t) = rename f $ rename t
    1.70 -          | rename(t) = t;
    1.71 -        fun strip_ren Ai = strip_apply rename (Ai,B)
    1.72 +          | rename (f $ t) = rename f $ rename t
    1.73 +          | rename t = t;
    1.74 +        fun strip_ren f Ai = f rename B Ai
    1.75        in strip_ren end;
    1.76  
    1.77  (*Function to rename bounds/unknowns in the argument, lifted over B*)
    1.78 -fun rename_bvars(dpairs, tpairs, B) =
    1.79 -        rename_bvs(List.foldr Term.match_bvars [] dpairs, dpairs, tpairs, B);
    1.80 +fun rename_bvars dpairs =
    1.81 +  rename_bvs (List.foldr Term.match_bvars [] dpairs) dpairs;
    1.82  
    1.83  
    1.84  (*** RESOLUTION ***)
    1.85 @@ -1640,9 +1657,11 @@
    1.86       fun newAs(As0, n, dpairs, tpairs) =
    1.87         let val (As1, rder') =
    1.88           if not lifted then (As0, rder)
    1.89 -         else (map (rename_bvars(dpairs,tpairs,B)) As0,
    1.90 -           deriv_rule1 (Proofterm.map_proof_terms
    1.91 -             (rename_bvars (dpairs, tpairs, Bound 0)) I) rder);
    1.92 +         else
    1.93 +           let val rename = rename_bvars dpairs tpairs B As0
    1.94 +           in (map (rename strip_apply) As0,
    1.95 +             deriv_rule1 (Proofterm.map_proof_terms (rename K) I) rder)
    1.96 +           end;
    1.97         in (map (if flatten then (Logic.flatten_params n) else I) As1, As1, rder', n)
    1.98            handle TERM _ =>
    1.99            raise THM("bicompose: 1st premise", 0, [orule])