# HG changeset patch
# User traytel
# Date 1365192522 -7200
# Node ID d602caf11e487f14755a208634bff73e41e2e14c
# Parent  18bbc78888aa8a6e6f221b91a95ab7c1eade2d35
tuned whitespace

diff -r 18bbc78888aa -r d602caf11e48 src/HOL/Tools/case_translation.ML
--- a/src/HOL/Tools/case_translation.ML	Thu Apr 04 18:48:40 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML	Fri Apr 05 22:08:42 2013 +0200
@@ -410,12 +410,12 @@
 fun check_case ctxt =
   let
     fun decode_case (Const (@{const_name case_guard}, _) $ (t $ u)) =
-        make_case ctxt Error Name.context (decode_case u) (decode_cases t)
-    | decode_case (t $ u) = decode_case t $ decode_case u
-    | decode_case (Abs (x, T, u)) =
-        let val (x', u') = Term.dest_abs (x, T, u);
-        in Term.absfree (x', T) (decode_case u') end
-    | decode_case t = t;
+          make_case ctxt Error Name.context (decode_case u) (decode_cases t)
+      | decode_case (t $ u) = decode_case t $ decode_case u
+      | decode_case (Abs (x, T, u)) =
+          let val (x', u') = Term.dest_abs (x, T, u);
+          in Term.absfree (x', T) (decode_case u') end
+      | decode_case t = t;
   in
     map decode_case
   end;