src/HOL/BNF/Tools/bnf_ctr_sugar.ML

                   val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs));
 
                   val half_goalss = map mk_goal half_pairss;
                   val half_thmss =
                     map3 (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] =>
-                        fn disc_thm => [prove (mk_half_disc_exclude_tac m discD disc_thm) goal])
+                        fn disc_thm => [prove (mk_half_disc_exclude_tac lthy m discD disc_thm) goal])
                       half_goalss half_pairss (flat disc_thmss');
 
                   val other_half_goalss = map (mk_goal o map swap) half_pairss;
                   val other_half_thmss =
                     map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss