diff -r b5fbe9837aee -r 0262155d2743 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Fri Mar 24 18:30:17 2023 +0000
+++ b/src/Tools/Code/code_ml.ML	Fri Mar 24 18:30:17 2023 +0000
@@ -129,7 +129,7 @@
           if wanted < 2 orelse length ts = wanted
           then (str o deresolve) sym
             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
-          else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.satisfied_application wanted app)]
+          else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.saturated_application wanted app)]
         end
       else if is_pseudo_fun sym
         then (str o deresolve) sym @@ str "()"
@@ -452,7 +452,7 @@
           if length ts = wanted
           then (str o deresolve) sym
             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
-          else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.satisfied_application wanted app)]
+          else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.saturated_application wanted app)]
         end
       else if is_pseudo_fun sym
         then (str o deresolve) sym @@ str "()"