equal
deleted
inserted
replaced
364 | _ => I) pat []; |
364 | _ => I) pat []; |
365 |
365 |
366 fun make_case ctxt config used x clauses = |
366 fun make_case ctxt config used x clauses = |
367 let |
367 let |
368 fun string_of_clause (pat, rhs) = |
368 fun string_of_clause (pat, rhs) = |
369 (case try (fn () => (* FIXME may crash!? *) |
369 Syntax.unparse_term ctxt |
370 Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs)) () |
370 (Term.list_comb (Syntax.const @{syntax_const "_case1"}, |
371 of |
371 Syntax.uncheck_terms ctxt [pat, rhs])) |
372 SOME s => s |
372 |> Pretty.string_of; |
373 | NONE => Markup.markup Markup.intensify "<malformed>"); |
|
374 |
373 |
375 val _ = map (no_repeat_vars ctxt o fst) clauses; |
374 val _ = map (no_repeat_vars ctxt o fst) clauses; |
376 val rows = map_index (fn (i, (pat, rhs)) => (([], [pat]), (rhs, i))) clauses; |
375 val rows = map_index (fn (i, (pat, rhs)) => (([], [pat]), (rhs, i))) clauses; |
377 val rangeT = |
376 val rangeT = |
378 (case distinct (op =) (map (fastype_of o snd) clauses) of |
377 (case distinct (op =) (map (fastype_of o snd) clauses) of |