tuned whitespace;
authorwenzelm
Tue Aug 09 21:48:36 2011 +0200 (2011-08-09 ago)
changeset 441002cf62c4e6c7a
parent 44099 5e14f591515e
child 44101 202d2f56560c
tuned whitespace;
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/proofterm.ML	Tue Aug 09 17:33:17 2011 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Tue Aug 09 21:48:36 2011 +0200
     1.3 @@ -881,23 +881,25 @@
     1.4    let
     1.5      val f = Envir.beta_norm f;
     1.6      val g = Envir.beta_norm g;
     1.7 -    val prf =  if check_comb prf1 then
     1.8 +    val prf =
     1.9 +      if check_comb prf1 then
    1.10          combination_axm % NONE % NONE
    1.11 -      else (case prf1 of
    1.12 +      else
    1.13 +        (case prf1 of
    1.14            PAxm ("Pure.reflexive", _, _) % _ =>
    1.15              combination_axm %> remove_types f % NONE
    1.16          | _ => combination_axm %> remove_types f %> remove_types g)
    1.17    in
    1.18      (case T of
    1.19 -       Type ("fun", _) => prf %
    1.20 -         (case head_of f of
    1.21 -            Abs _ => SOME (remove_types t)
    1.22 -          | Var _ => SOME (remove_types t)
    1.23 -          | _ => NONE) %
    1.24 -         (case head_of g of
    1.25 -            Abs _ => SOME (remove_types u)
    1.26 -          | Var _ => SOME (remove_types u)
    1.27 -          | _ => NONE) %% prf1 %% prf2
    1.28 +      Type ("fun", _) => prf %
    1.29 +        (case head_of f of
    1.30 +          Abs _ => SOME (remove_types t)
    1.31 +        | Var _ => SOME (remove_types t)
    1.32 +        | _ => NONE) %
    1.33 +        (case head_of g of
    1.34 +           Abs _ => SOME (remove_types u)
    1.35 +        | Var _ => SOME (remove_types u)
    1.36 +        | _ => NONE) %% prf1 %% prf2
    1.37       | _ => prf % NONE % NONE %% prf1 %% prf2)
    1.38    end;
    1.39