--- a/src/Tools/Code/code_scala.ML Sun Apr 03 14:48:55 2022 +0100
+++ b/src/Tools/Code/code_scala.ML Sun Apr 03 09:07:37 2022 +0000
@@ -160,8 +160,8 @@
fun print_match_val ((pat, ty), t) vars =
vars
|> print_bind tyvars some_thm BR pat
- |>> (fn p => (false, concat [str "val", constraint p (print_typ tyvars NOBR ty),
- str "=", print_term tyvars false some_thm vars NOBR t]));
+ |>> (fn p => (false, concat [str "val", p, str "=",
+ constraint (print_term tyvars false some_thm vars NOBR t) (print_typ tyvars NOBR ty)]));
fun print_match_seq t vars =
((true, print_term tyvars false some_thm vars NOBR t), vars);
fun print_match is_first ((IVar NONE, ty), t) =