src/Pure/Isar/rule_cases.ML

 
 fun lookup_consumes th =
   (case AList.lookup (op =) (Thm.get_tags th) consumes_tagN of
     NONE => NONE
   | SOME s =>
-      (case Lexicon.read_nat s of SOME n => SOME n
+      (case Lexicon.read_nat s of
+        SOME n => SOME n
       | _ => raise THM ("Malformed 'consumes' tag of theorem", 0, [th])));
 
 fun get_consumes th = the_default 0 (lookup_consumes th);
 
 fun put_consumes NONE th = th

 
 fun lookup_constraints th =
   (case AList.lookup (op =) (Thm.get_tags th) constraints_tagN of
     NONE => NONE
   | SOME s =>
-      (case Lexicon.read_nat s of SOME n => SOME n
+      (case Lexicon.read_nat s of
+        SOME n => SOME n
       | _ => raise THM ("Malformed 'constraints' tag of theorem", 0, [th])));
 
 fun get_constraints th = the_default 0 (lookup_constraints th);
 
 fun put_constraints NONE th = th

   these (get_first (get_case_concl name) (Thm.get_tags th));
 
 fun save_case_concls th =
   let val concls = Thm.get_tags th |> map_filter
     (fn (a, b) =>
-      if a = case_concl_tagN then (case explode_args b of c :: cs => SOME (c, cs) | _ => NONE)
+      if a = case_concl_tagN
+      then (case explode_args b of c :: cs => SOME (c, cs) | _ => NONE)
       else NONE)
   in fold add_case_concl concls end;
 
 fun case_conclusion concl = Thm.mixed_attribute (apsnd (add_case_concl concl));
 

     val n = get_consumes th;
     val cases =
       (case lookup_case_names th of
         NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n))
       | SOME names => map (fn name => (name, get_case_concls th name)) names);
-    val cases_hyps = (case lookup_cases_hyp_names th of
+    val cases_hyps =
+      (case lookup_cases_hyp_names th of
         NONE => replicate (length cases) []
       | SOME names => names);
     fun regroup ((name,concls),hyps) = ((name,hyps),concls)
   in (map regroup (cases ~~ cases_hyps), n) end;