src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 75017 30ccc472d486
parent 75016 873b581fd690
child 75020 b087610592b4
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -57,7 +57,7 @@
      goal : thm,
      subgoal : int,
      subgoal_count : int,
-     factss : (string * fact list) list,
+     facts : string * fact list,
      found_proof : unit -> unit}
 
   type prover_result =
@@ -185,7 +185,7 @@
    goal : thm,
    subgoal : int,
    subgoal_count : int,
-   factss : (string * fact list) list,
+   facts : string * fact list,
    found_proof : unit -> unit}
 
 type prover_result =