1.1 --- a/src/FOLP/hypsubst.ML	Sat Aug 29 10:50:04 2009 +0200
     1.2 +++ b/src/FOLP/hypsubst.ML	Sat Aug 29 12:01:25 2009 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4    val inspect_pair        : bool -> term * term -> thm
     1.5    end;
     1.6  
     1.7 -functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
     1.8 +functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
     1.9  struct
    1.10  
    1.11  local open Data in
    1.12 @@ -43,13 +43,13 @@
    1.13      but how could we check for this?*)
    1.14  fun inspect_pair bnd (t,u) =
    1.15    case (Envir.eta_contract t, Envir.eta_contract u) of
    1.16 -       (Bound i, _) => if loose(i,u) then raise Match 
    1.17 +       (Bound i, _) => if loose(i,u) then raise Match
    1.18                         else sym         (*eliminates t*)
    1.19 -     | (_, Bound i) => if loose(i,t) then raise Match 
    1.20 +     | (_, Bound i) => if loose(i,t) then raise Match
    1.21                         else asm_rl      (*eliminates u*)
    1.22 -     | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match 
    1.23 +     | (Free _, _) => if bnd orelse Logic.occs(t,u) then raise Match
    1.24                        else sym          (*eliminates t*)
    1.25 -     | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match 
    1.26 +     | (_, Free _) => if bnd orelse Logic.occs(u,t) then raise Match
    1.27                        else asm_rl       (*eliminates u*)
    1.28       | _ => raise Match;
    1.29  
    1.30 @@ -58,7 +58,7 @@
    1.31     the rule asm_rl (resp. sym). *)
    1.32  fun eq_var bnd =
    1.33    let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
    1.34 -        | eq_var_aux k (Const("==>",_) $ A $ B) = 
    1.35 +        | eq_var_aux k (Const("==>",_) $ A $ B) =
    1.36                ((k, inspect_pair bnd (dest_eq A))
    1.37                        (*Exception Match comes from inspect_pair or dest_eq*)
    1.38                 handle Match => eq_var_aux (k+1) B)
    1.39 @@ -70,13 +70,13 @@
    1.40  fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
    1.41        let val n = length(Logic.strip_assums_hyp Bi) - 1
    1.42            val (k,symopt) = eq_var bnd Bi
    1.43 -      in 
    1.44 +      in
    1.45           DETERM
    1.46             (EVERY [REPEAT_DETERM_N k (etac rev_mp i),
    1.47 -		   etac revcut_rl i,
    1.48 -		   REPEAT_DETERM_N (n-k) (etac rev_mp i),
    1.49 -		   etac (symopt RS subst) i,
    1.50 -		   REPEAT_DETERM_N n (rtac imp_intr i)])
    1.51 +                   etac revcut_rl i,
    1.52 +                   REPEAT_DETERM_N (n-k) (etac rev_mp i),
    1.53 +                   etac (symopt RS subst) i,
    1.54 +                   REPEAT_DETERM_N n (rtac imp_intr i)])
    1.55        end
    1.56        handle THM _ => no_tac | EQ_VAR => no_tac);
    1.57