src/Tools/Code/code_ml.ML

       if is_constr sym then
         let val wanted = length dom in
           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 "()"
       else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
         @ map (print_term is_pseudo_fun some_thm vars BR) ts

       if is_constr sym then
         let val wanted = length dom in
           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 "()"
       else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
         @ map (print_term is_pseudo_fun some_thm vars BR) ts