# 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 *)