# HG changeset patch
# User traytel
# Date 1374228031 -7200
# Node ID c12602c1b13b0ee6d57a74bcc8ef40583b460c56
# Parent  b824497c8e8670f4a77b1cfc9a93e259033b71ed
do not apply string_of_term to dummy-typed syntactic constants (ensures that uncheck phases work on well-typed terms)

diff -r b824497c8e86 -r c12602c1b13b src/HOL/Tools/case_translation.ML
--- a/src/HOL/Tools/case_translation.ML	Thu Jul 18 23:13:44 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML	Fri Jul 19 12:00:31 2013 +0200
@@ -366,11 +366,10 @@
 fun make_case ctxt config used x clauses =
   let
     fun string_of_clause (pat, rhs) =
-      (case try (fn () => (* FIXME may crash!? *)
-        Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs)) ()
-       of
-        SOME s => s
-      | NONE => Markup.markup Markup.intensify "<malformed>");
+      Syntax.unparse_term ctxt
+        (Term.list_comb (Syntax.const @{syntax_const "_case1"},
+          Syntax.uncheck_terms ctxt [pat, rhs]))
+      |> Pretty.string_of;
 
     val _ = map (no_repeat_vars ctxt o fst) clauses;
     val rows = map_index (fn (i, (pat, rhs)) => (([], [pat]), (rhs, i))) clauses;