# HG changeset patch
# User haftmann
# Date 1501757399 -7200
# Node ID f44f7cf3d1a1df04afc7183c18c6c5a8f67ccd23
# Parent  9eb8a2d07852874eae6d2b74bae87811655ac033
corrected slip

diff -r 9eb8a2d07852 -r f44f7cf3d1a1 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Aug 03 12:49:58 2017 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Aug 03 12:49:59 2017 +0200
@@ -83,7 +83,6 @@
           let
             val (vs_tys, body) = Code_Thingol.unfold_abs t;
             val (ps, vars') = fold_map (print_abs_head tyvars) vs_tys vars;
-            val vars' = intro_vars (map_filter fst vs_tys) vars;
           in
             brackets (ps @| print_term tyvars false some_thm vars' NOBR body)
           end