src/Pure/raw_simplifier.ML

           if fo then Thm.first_order_match (elhs', eta_t')
           else Thm.match (elhs', eta_t');
         val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
         val prop' = Thm.prop_of thm';
         val unconditional = (Logic.count_prems prop' = 0);
-        val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
+        val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop');
       in
         if perm andalso not (termless (rhs', lhs'))
-        then (trace_named_thm ctxt (fn () => "Cannot apply permutative rewrite rule") (thm, name);
-              trace_thm ctxt (fn () => "Term does not become smaller:") thm'; NONE)
-        else (trace_named_thm ctxt (fn () => "Applying instance of rewrite rule") (thm, name);
-           if unconditional
-           then
-             (trace_thm ctxt (fn () => "Rewriting:") thm';
+        then
+         (trace_named_thm ctxt (fn () => "Cannot apply permutative rewrite rule") (thm, name);
+          trace_thm ctxt (fn () => "Term does not become smaller:") thm';
+          NONE)
+        else
+         (trace_named_thm ctxt (fn () => "Applying instance of rewrite rule") (thm, name);
+          if unconditional
+          then
+           (trace_thm ctxt (fn () => "Rewriting:") thm';
+            let
+              val lr = Logic.dest_equals prop;
+              val SOME thm'' = check_conv ctxt false eta_thm thm';
+            in SOME (thm'', uncond_skel (congs, lr)) end)
+          else
+           (trace_thm ctxt (fn () => "Trying to rewrite:") thm';
+            if simp_depth ctxt > Config.get ctxt simp_depth_limit
+            then
               let
-                val lr = Logic.dest_equals prop;
-                val SOME thm'' = check_conv ctxt false eta_thm thm';
-              in SOME (thm'', uncond_skel (congs, lr)) end)
-           else
-             (trace_thm ctxt (fn () => "Trying to rewrite:") thm';
-              if simp_depth ctxt > Config.get ctxt simp_depth_limit
-              then
-                let
-                  val s = "simp_depth_limit exceeded - giving up";
-                  val _ = trace ctxt false (fn () => s);
-                  val _ = Context_Position.if_visible ctxt warning s;
-                in NONE end
-              else
-              case prover ctxt thm' of
+                val s = "simp_depth_limit exceeded - giving up";
+                val _ = trace ctxt false (fn () => s);
+                val _ = Context_Position.if_visible ctxt warning s;
+              in NONE end
+            else
+              (case prover ctxt thm' of
                 NONE => (trace_thm ctxt (fn () => "FAILED") thm'; NONE)
               | SOME thm2 =>
                   (case check_conv ctxt true eta_thm thm2 of
                     NONE => NONE
                   | SOME thm2' =>
                       let
                         val concl = Logic.strip_imp_concl prop;
                         val lr = Logic.dest_equals concl;
-                      in SOME (thm2', cond_skel (congs, lr)) end)))
+                      in SOME (thm2', cond_skel (congs, lr)) end))))
       end;
 
     fun rews [] = NONE
       | rews (rrule :: rrules) =
           let val opt = rew rrule handle Pattern.MATCH => NONE
-          in case opt of NONE => rews rrules | some => some end;
+          in (case opt of NONE => rews rrules | some => some) end;
 
     fun sort_rrules rrs =
       let
         fun is_simple ({thm, ...}: rrule) =
           (case Thm.prop_of thm of

 
     fun proc_rews [] = NONE
       | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
           if Pattern.matches (Proof_Context.theory_of ctxt) (Thm.term_of lhs, Thm.term_of t) then
             (debug_term ctxt false (fn () => "Trying procedure " ^ quote name ^ " on:") eta_t;
-             case proc ctxt eta_t' of
+             (case proc ctxt eta_t' of
                NONE => (debug ctxt false (fn () => "FAILED"); proc_rews ps)
              | SOME raw_thm =>
                  (trace_thm ctxt (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:")
                    raw_thm;
                   (case rews (mk_procrule ctxt raw_thm) of
                     NONE => (trace_cterm ctxt true (fn () => "IGNORED result of simproc " ^ quote name ^
                       " -- does not match") t; proc_rews ps)
-                  | some => some)))
+                  | some => some))))
           else proc_rews ps;
   in
     (case eta_t of
       Abs _ $ _ => SOME (Thm.transitive eta_thm (Thm.beta_conversion false eta_t'), skel0)
     | _ =>

   apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong)));
 
 fun transitive1 NONE NONE = NONE
   | transitive1 (SOME thm1) NONE = SOME thm1
   | transitive1 NONE (SOME thm2) = SOME thm2
-  | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2)
+  | transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2);
 
 fun transitive2 thm = transitive1 (SOME thm);
 fun transitive3 thm = transitive1 thm o SOME;
 
 fun bottomc ((simprem, useprem, mutsimp), prover, maxidx) =
   let
     fun botc skel ctxt t =
-          if is_Var skel then NONE
-          else
-          (case subc skel ctxt t of
-             some as SOME thm1 =>
-               (case rewritec (prover, maxidx) ctxt (Thm.rhs_of thm1) of
-                  SOME (thm2, skel2) =>
-                    transitive2 (Thm.transitive thm1 thm2)
-                      (botc skel2 ctxt (Thm.rhs_of thm2))
-                | NONE => some)
-           | NONE =>
-               (case rewritec (prover, maxidx) ctxt t of
-                  SOME (thm2, skel2) => transitive2 thm2
+      if is_Var skel then NONE
+      else
+        (case subc skel ctxt t of
+           some as SOME thm1 =>
+             (case rewritec (prover, maxidx) ctxt (Thm.rhs_of thm1) of
+                SOME (thm2, skel2) =>
+                  transitive2 (Thm.transitive thm1 thm2)
                     (botc skel2 ctxt (Thm.rhs_of thm2))
-                | NONE => NONE))
+              | NONE => some)
+         | NONE =>
+             (case rewritec (prover, maxidx) ctxt t of
+                SOME (thm2, skel2) => transitive2 thm2
+                  (botc skel2 ctxt (Thm.rhs_of thm2))
+              | NONE => NONE))
 
     and try_botc ctxt t =
-          (case botc skel0 ctxt t of
-            SOME trec1 => trec1
-          | NONE => (Thm.reflexive t))
+      (case botc skel0 ctxt t of
+        SOME trec1 => trec1
+      | NONE => Thm.reflexive t)
 
     and subc skel ctxt t0 =
         let val Simpset ({bounds, ...}, {congs, ...}) = simpset_of ctxt in
           (case term_of t0 of
               Abs (a, T, _) =>

                       if b <> b' then
                         warning ("Simplifier: renamed bound variable " ^
                           quote b ^ " to " ^ quote b' ^ Position.here (Position.thread_data ()))
                       else ();
                     val ctxt' = add_bound ((b', T), a) ctxt;
-                    val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
+                    val skel' = (case skel of Abs (_, _, sk) => sk | _ => skel0);
                 in
                   (case botc skel' ctxt' t' of
                     SOME thm => SOME (Thm.abstract_rule a v thm)
                   | NONE => NONE)
                 end
-            | t $ _ => (case t of
+            | t $ _ =>
+              (case t of
                 Const ("==>", _) $ _  => impc t0 ctxt
               | Abs _ =>
                   let val thm = Thm.beta_conversion false t0
-                  in case subc skel0 ctxt (Thm.rhs_of thm) of
-                       NONE => SOME thm
-                     | SOME thm' => SOME (Thm.transitive thm thm')
+                  in
+                    (case subc skel0 ctxt (Thm.rhs_of thm) of
+                      NONE => SOME thm
+                    | SOME thm' => SOME (Thm.transitive thm thm'))
                   end
               | _  =>
                   let fun appc () =
                         let
-                          val (tskel, uskel) = case skel of
+                          val (tskel, uskel) =
+                            (case skel of
                               tskel $ uskel => (tskel, uskel)
-                            | _ => (skel0, skel0);
-                          val (ct, cu) = Thm.dest_comb t0
+                            | _ => (skel0, skel0));
+                          val (ct, cu) = Thm.dest_comb t0;
                         in
-                        (case botc tskel ctxt ct of
-                           SOME thm1 =>
-                             (case botc uskel ctxt cu of
+                          (case botc tskel ctxt ct of
+                            SOME thm1 =>
+                              (case botc uskel ctxt cu of
                                 SOME thm2 => SOME (Thm.combination thm1 thm2)
                               | NONE => SOME (Thm.combination thm1 (Thm.reflexive cu)))
-                         | NONE =>
-                             (case botc uskel ctxt cu of
+                          | NONE =>
+                              (case botc uskel ctxt cu of
                                 SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1)
                               | NONE => NONE))
                         end
-                      val (h, ts) = strip_comb t
-                  in case cong_name h of
-                       SOME a =>
-                         (case AList.lookup (op =) (fst congs) a of
-                            NONE => appc ()
-                          | SOME cong =>
+                      val (h, ts) = strip_comb t;
+                  in
+                    (case cong_name h of
+                      SOME a =>
+                        (case AList.lookup (op =) (fst congs) a of
+                           NONE => appc ()
+                        | SOME cong =>
      (*post processing: some partial applications h t1 ... tj, j <= length ts,
        may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
-                             (let
-                                val thm = congc (prover ctxt) ctxt maxidx cong t0;
-                                val t = the_default t0 (Option.map Thm.rhs_of thm);
-                                val (cl, cr) = Thm.dest_comb t
-                                val dVar = Var(("", 0), dummyT)
-                                val skel =
-                                  list_comb (h, replicate (length ts) dVar)
-                              in case botc skel ctxt cl of
-                                   NONE => thm
-                                 | SOME thm' => transitive3 thm
-                                     (Thm.combination thm' (Thm.reflexive cr))
-                              end handle Pattern.MATCH => appc ()))
-                     | _ => appc ()
+                           (let
+                              val thm = congc (prover ctxt) ctxt maxidx cong t0;
+                              val t = the_default t0 (Option.map Thm.rhs_of thm);
+                              val (cl, cr) = Thm.dest_comb t
+                              val dVar = Var(("", 0), dummyT)
+                              val skel =
+                                list_comb (h, replicate (length ts) dVar)
+                            in
+                              (case botc skel ctxt cl of
+                                NONE => thm
+                              | SOME thm' =>
+                                  transitive3 thm (Thm.combination thm' (Thm.reflexive cr)))
+                            end handle Pattern.MATCH => appc ()))
+                     | _ => appc ())
                   end)
             | _ => NONE)
         end
     and impc ct ctxt =
-      if mutsimp then mut_impc0 [] ct [] [] ctxt else nonmut_impc ct ctxt
+      if mutsimp then mut_impc0 [] ct [] [] ctxt
+      else nonmut_impc ct ctxt
 
     and rules_of_prem ctxt prem =
       if maxidx_of_term (term_of prem) <> ~1
       then (trace_cterm ctxt true
         (fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:")

       let
         val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
         val eq' = Thm.implies_elim (Thm.instantiate
           ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
           (Thm.implies_intr prem eq)
-      in if not r then eq' else
-        let
-          val (prem', concl) = Thm.dest_implies lhs;
-          val (prem'', _) = Thm.dest_implies rhs
-        in Thm.transitive (Thm.transitive
-          (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
-             Drule.swap_prems_eq) eq')
-          (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)])
-             Drule.swap_prems_eq)
-        end
+      in
+        if not r then eq'
+        else
+          let
+            val (prem', concl) = Thm.dest_implies lhs;
+            val (prem'', _) = Thm.dest_implies rhs
+          in Thm.transitive (Thm.transitive
+            (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
+               Drule.swap_prems_eq) eq')
+            (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)])
+               Drule.swap_prems_eq)
+          end
       end
 
     and rebuild [] _ _ _ _ eq = eq
       | rebuild (prem :: prems) concl (_ :: rrss) (_ :: asms) ctxt eq =
           let

            else rebuild prems' concl rrss' asms' ctxt
              (botc skel0 (add_rrules (rev rrss', rev asms') ctxt) concl))
 
       | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms)
           prems' rrss' asms' eqns ctxt changed k =
-        case (if k = 0 then NONE else botc skel0 (add_rrules
+        (case (if k = 0 then NONE else botc skel0 (add_rrules
           (rev rrss' @ rrss, rev asms' @ asms) ctxt) prem) of
             NONE => mut_impc prems concl rrss asms (prem :: prems')
               (rrs :: rrss') (asm :: asms') (NONE :: eqns) ctxt changed
               (if k = 0 then 0 else k - 1)
-          | SOME eqn =>
+        | SOME eqn =>
             let
               val prem' = Thm.rhs_of eqn;
               val tprems = map term_of prems;
               val i = 1 + fold Integer.max (map (fn p =>
                 find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1;
               val (rrs', asm') = rules_of_prem ctxt prem';
-            in mut_impc prems concl rrss asms (prem' :: prems')
-              (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
-                (take i prems)
-                (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies
-                  (drop i prems, concl))))) :: eqns)
-                  ctxt (length prems') ~1
-            end
-
-     (*legacy code - only for backwards compatibility*)
+            in
+              mut_impc prems concl rrss asms (prem' :: prems')
+                (rrs' :: rrss') (asm' :: asms')
+                (SOME (fold_rev (disch true)
+                  (take i prems)
+                  (Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies
+                    (drop i prems, concl))))) :: eqns)
+                ctxt (length prems') ~1
+            end)
+
+    (*legacy code -- only for backwards compatibility*)
     and nonmut_impc ct ctxt =
       let
         val (prem, conc) = Thm.dest_implies ct;
         val thm1 = if simprem then botc skel0 ctxt prem else NONE;
         val prem1 = the_default prem (Option.map Thm.rhs_of thm1);

               (case thm1 of
                 NONE => SOME thm2'
               | SOME thm1' =>
                  SOME (Thm.transitive (Drule.imp_cong_rule thm1' (Thm.reflexive conc)) thm2'))
             end)
-      end
-
- in try_botc end;
+      end;
+
+  in try_botc end;
 
 
 (* Meta-rewriting: rewrites t to u and returns the theorem t==u *)
 
 (*