src/HOL/BNF/Tools/bnf_ctr_sugar.ML

       let
         val ([exhaust_thm], (inject_thmss, half_distinct_thmss)) = (hd thmss, chop n (tl thmss));
 
         val inject_thms = flat inject_thmss;
 
-        val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
+        val rho_As = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As);
 
         fun inst_thm t thm =
           Drule.instantiate' [] [SOME (certify lthy t)]
-            (Thm.instantiate (Tinst, []) (Drule.zero_var_indexes thm));
+            (Thm.instantiate (rho_As, []) (Drule.zero_var_indexes thm));
 
         val uexhaust_thm = inst_thm u exhaust_thm;
 
         val exhaust_cases = map base_name_of_ctr ctrs;