src/HOL/Tools/Function/lexicographic_order.ML

--- a/src/HOL/Tools/Function/lexicographic_order.ML	Mon Mar 17 16:29:48 2025 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Tue Mar 18 08:41:07 2025 +0100
@@ -203,7 +203,7 @@
           st |>
           (PRIMITIVE (infer_instantiate ctxt [(#1 (dest_Var rel), Thm.cterm_of ctxt relation)])
             THEN (REPEAT (resolve_tac ctxt @{thms wf_mlex} 1))
-            THEN (resolve_tac ctxt @{thms wf_on_def} 1)
+            THEN (resolve_tac ctxt @{thms wf_on_bot} 1)
             THEN EVERY (map (prove_row_tac ctxt) clean_table))
         end
   end) 1 st;