--- a/src/Tools/induct.ML	Wed Jan 22 21:35:05 2025 +0100
+++ b/src/Tools/induct.ML	Wed Jan 22 22:22:19 2025 +0100
@@ -120,7 +120,7 @@
 
 in
 
-fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle List.Empty =>
+fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.take_prems_of 1 thm)))) handle List.Empty =>
   raise THM ("No variables in major premise of rule", 0, [thm]);
 
 val left_var_concl = concl_var hd;