tuned whitespace;
authorwenzelm
Thu Dec 12 16:56:53 2013 +0100 (2013-12-12)
changeset 54727a806e7251cf0
parent 54726 5285805af26c
child 54728 445e7947c6b5
tuned whitespace;
src/Pure/raw_simplifier.ML
     1.1 --- a/src/Pure/raw_simplifier.ML	Thu Dec 12 16:25:21 2013 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Thu Dec 12 16:56:53 2013 +0100
     1.3 @@ -1114,25 +1114,26 @@
     1.4                      | SOME thm' => SOME (Thm.transitive thm thm'))
     1.5                    end
     1.6                | _  =>
     1.7 -                  let fun appc () =
     1.8 -                        let
     1.9 -                          val (tskel, uskel) =
    1.10 -                            (case skel of
    1.11 -                              tskel $ uskel => (tskel, uskel)
    1.12 -                            | _ => (skel0, skel0));
    1.13 -                          val (ct, cu) = Thm.dest_comb t0;
    1.14 -                        in
    1.15 -                          (case botc tskel ctxt ct of
    1.16 -                            SOME thm1 =>
    1.17 -                              (case botc uskel ctxt cu of
    1.18 -                                SOME thm2 => SOME (Thm.combination thm1 thm2)
    1.19 -                              | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu)))
    1.20 -                          | NONE =>
    1.21 -                              (case botc uskel ctxt cu of
    1.22 -                                SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1)
    1.23 -                              | NONE => NONE))
    1.24 -                        end
    1.25 -                      val (h, ts) = strip_comb t;
    1.26 +                  let
    1.27 +                    fun appc () =
    1.28 +                      let
    1.29 +                        val (tskel, uskel) =
    1.30 +                          (case skel of
    1.31 +                            tskel $ uskel => (tskel, uskel)
    1.32 +                          | _ => (skel0, skel0));
    1.33 +                        val (ct, cu) = Thm.dest_comb t0;
    1.34 +                      in
    1.35 +                        (case botc tskel ctxt ct of
    1.36 +                          SOME thm1 =>
    1.37 +                            (case botc uskel ctxt cu of
    1.38 +                              SOME thm2 => SOME (Thm.combination thm1 thm2)
    1.39 +                            | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu)))
    1.40 +                        | NONE =>
    1.41 +                            (case botc uskel ctxt cu of
    1.42 +                              SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1)
    1.43 +                            | NONE => NONE))
    1.44 +                      end;
    1.45 +                    val (h, ts) = strip_comb t;
    1.46                    in
    1.47                      (case cong_name h of
    1.48                        SOME a =>
    1.49 @@ -1177,20 +1178,22 @@
    1.50      and disch r prem eq =
    1.51        let
    1.52          val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
    1.53 -        val eq' = Thm.implies_elim (Thm.instantiate
    1.54 -          ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
    1.55 -          (Thm.implies_intr prem eq)
    1.56 +        val eq' =
    1.57 +          Thm.implies_elim
    1.58 +            (Thm.instantiate ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
    1.59 +            (Thm.implies_intr prem eq);
    1.60        in
    1.61          if not r then eq'
    1.62          else
    1.63            let
    1.64              val (prem', concl) = Thm.dest_implies lhs;
    1.65 -            val (prem'', _) = Thm.dest_implies rhs
    1.66 -          in Thm.transitive (Thm.transitive
    1.67 -            (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
    1.68 -               Drule.swap_prems_eq) eq')
    1.69 -            (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)])
    1.70 -               Drule.swap_prems_eq)
    1.71 +            val (prem'', _) = Thm.dest_implies rhs;
    1.72 +          in
    1.73 +            Thm.transitive
    1.74 +              (Thm.transitive
    1.75 +                (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)]) Drule.swap_prems_eq)
    1.76 +                eq')
    1.77 +              (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)]) Drule.swap_prems_eq)
    1.78            end
    1.79        end
    1.80  
    1.81 @@ -1200,19 +1203,19 @@
    1.82              val ctxt' = add_rrules (rev rrss, rev asms) ctxt;
    1.83              val concl' =
    1.84                Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq));
    1.85 -            val dprem = Option.map (disch false prem)
    1.86 +            val dprem = Option.map (disch false prem);
    1.87            in
    1.88              (case rewritec (prover, maxidx) ctxt' concl' of
    1.89                NONE => rebuild prems concl' rrss asms ctxt (dprem eq)
    1.90 -            | SOME (eq', _) => transitive2 (fold (disch false)
    1.91 -                  prems (the (transitive3 (dprem eq) eq')))
    1.92 -                (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ctxt))
    1.93 +            | SOME (eq', _) =>
    1.94 +                transitive2 (fold (disch false) prems (the (transitive3 (dprem eq) eq')))
    1.95 +                  (mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ctxt))
    1.96            end
    1.97  
    1.98      and mut_impc0 prems concl rrss asms ctxt =
    1.99        let
   1.100          val prems' = strip_imp_prems concl;
   1.101 -        val (rrss', asms') = split_list (map (rules_of_prem ctxt) prems')
   1.102 +        val (rrss', asms') = split_list (map (rules_of_prem ctxt) prems');
   1.103        in
   1.104          mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss')
   1.105            (asms @ asms') [] [] [] [] ctxt ~1 ~1