do not apply string_of_term to dummy-typed syntactic constants (ensures that uncheck phases work on well-typed terms)
--- 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;