# HG changeset patch
# User haftmann
# Date 1388534730 -3600
# Node ID 6edabf38d929bc73e96fb3efdeb12fb3c347a274
# Parent  83bf0ae03c507edd8482baf423e252a5298ceb9b
tuned whitespace

diff -r 83bf0ae03c50 -r 6edabf38d929 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Jan 01 01:05:30 2014 +0100
+++ b/src/Pure/Isar/code.ML	Wed Jan 01 01:05:30 2014 +0100
@@ -1096,7 +1096,8 @@
     | 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)