# HG changeset patch
# User wenzelm
# Date 1396439612 -7200
# Node ID 720414857a12959ddad06603ede683a4769994b2
# Parent  9f9f60f4dbbfa03c0fb0de5e6ff9797ccbae0b80
tuned whitespace;

diff -r 9f9f60f4dbbf -r 720414857a12 src/HOL/Tools/Ctr_Sugar/case_translation.ML
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Wed Apr 02 13:54:50 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Wed Apr 02 13:53:32 2014 +0200
@@ -599,7 +599,7 @@
   then map (fn t => if can Term.type_of t then strip_case_full ctxt true t else t) ts
   else ts;
 
-val _ = Context.>>  (Syntax_Phases.term_uncheck 1 "case" uncheck_case);
+val _ = Context.>> (Syntax_Phases.term_uncheck 1 "case" uncheck_case);
 
 
 (* outer syntax commands *)