--- a/src/Tools/Code/code_scala.ML Sun Mar 27 19:27:54 2022 +0000
+++ b/src/Tools/Code/code_scala.ML Mon Mar 28 12:54:09 2022 +0000
@@ -234,8 +234,8 @@
print_term tyvars false some_thm vars' NOBR t;
fun print_clause (eq as ((ts, _), (some_thm, _))) =
let
- val vars' = intro_vars ((fold o Code_Thingol.fold_varnames)
- (insert (op =)) ts []) vars1;
+ val vars' =
+ intro_vars (build (fold Code_Thingol.add_varnames ts)) vars1;
in
concat [str "case",
tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),