# HG changeset patch
# User wenzelm
# Date 1370089564 -7200
# Node ID da42b500a6aa37d107fb6f35ab8b117c9e238993
# Parent  b12f2cef3ee5d4374baa28d5c88525c6ebd85741
permissive uncheck -- allow printing of malformed terms (e.g. in error messages);

diff -r b12f2cef3ee5 -r da42b500a6aa src/HOL/Tools/case_translation.ML
--- a/src/HOL/Tools/case_translation.ML	Sat Jun 01 14:16:10 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML	Sat Jun 01 14:26:04 2013 +0200
@@ -559,7 +559,9 @@
 val show_cases = Attrib.setup_config_bool @{binding show_cases} (K true);
 
 fun uncheck_case ctxt ts =
-  if Config.get ctxt show_cases then map (strip_case_full ctxt true) ts else ts;
+  if Config.get ctxt show_cases
+  then map (fn t => if can Term.type_of t then strip_case_full ctxt true t else t) ts
+  else ts;
 
 val term_uncheck_setup =
   Context.theory_map (Syntax_Phases.term_uncheck 1 "case" uncheck_case);