--- 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;