1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 23 15:01:00 2020 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Sep 23 15:18:07 2020 +0200
     1.3 @@ -28,9 +28,9 @@
     1.4  
     1.5  open ATP_Util
     1.6  open ATP_Problem
     1.7 +open ATP_Problem_Generate
     1.8  open ATP_Proof
     1.9  open ATP_Proof_Reconstruct
    1.10 -open ATP_Waldmeister
    1.11  open Sledgehammer_Util
    1.12  open Sledgehammer_Proof_Methods
    1.13  open Sledgehammer_Isar_Proof
    1.14 @@ -62,8 +62,8 @@
    1.15  
    1.16  val skolemize_rules =
    1.17    [e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule,
    1.18 -   spass_skolemize_rule, vampire_skolemisation_rule,
    1.19 -   veriT_tmp_skolemize_rule, waldmeister_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule]
    1.20 +   spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule,
    1.21 +   zipperposition_cnf_rule]
    1.22  
    1.23  fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule)
    1.24  val is_maybe_ext_rule = is_ext_rule orf String.isPrefix satallax_tab_rule_prefix