src/Pure/Isar/code.ML

    of SOME (eqn, NONE) => gen_add_eqn false eqn thy
     | SOME ((thm, _), SOME tyco) => gen_add_abs_eqn (thm, tyco) thy
     | NONE => thy;
 
 fun del_eqn thm thy = case mk_eqn_liberal thy thm
- of SOME (thm, _) => let
+ of SOME (thm, _) =>
+      let
         fun del_eqn' (Default _) = initial_fun_spec
           | del_eqn' (Eqns eqns) =
               Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns)
           | del_eqn' spec = spec
       in change_fun_spec (const_eqn thy thm) del_eqn' thy end