src/HOL/Tools/res_atp.ML
changeset 21790 9d2761d09d91
parent 21690 552d20ff9a95
child 21858 05f57309170c
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Dec 12 12:03:46 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Dec 12 16:20:57 2006 +0100
     1.3 @@ -31,7 +31,6 @@
     1.4    val atp_method: (Proof.context -> thm list -> int -> tactic) ->
     1.5      Method.src -> Proof.context -> Proof.method
     1.6    val cond_rm_tmp: string -> unit
     1.7 -  val fol_keep_types: bool ref
     1.8    val hol_full_types: unit -> unit
     1.9    val hol_partial_types: unit -> unit
    1.10    val hol_const_types_only: unit -> unit
    1.11 @@ -135,7 +134,6 @@
    1.12  fun eproverLimit () = !eprover_time;
    1.13  fun spassLimit () = !spass_time;
    1.14  
    1.15 -val fol_keep_types = ResClause.keep_types;
    1.16  val hol_full_types = ResHolClause.full_types;
    1.17  val hol_partial_types = ResHolClause.partial_types;
    1.18  val hol_const_types_only = ResHolClause.const_types_only;
    1.19 @@ -741,16 +739,13 @@
    1.20          val user_cls = ResAxioms.cnf_rules_pairs user_rules
    1.21          val thy = ProofContext.theory_of ctxt
    1.22          val axclauses = make_unique (get_relevant_clauses thy cla_simp_atp_clauses user_cls goal_tms)
    1.23 -        val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
    1.24          val subs = tfree_classes_of_terms goal_tms
    1.25          and axtms = map (prop_of o #1) axclauses
    1.26          val supers = tvar_classes_of_terms axtms
    1.27          and tycons = type_consts_of_terms thy (goal_tms@axtms)
    1.28          (*TFrees in conjecture clauses; TVars in axiom clauses*)
    1.29 -        val classrel_clauses =
    1.30 -              if keep_types then ResClause.make_classrel_clauses thy subs supers
    1.31 -              else []
    1.32 -        val arity_clauses = if keep_types then ResClause.arity_clause_thy thy tycons supers else []
    1.33 +        val classrel_clauses = ResClause.make_classrel_clauses thy subs supers
    1.34 +        val arity_clauses = ResClause.arity_clause_thy thy tycons supers
    1.35          val writer = if dfg then dfg_writer else tptp_writer
    1.36          and file = atp_input_file()
    1.37          and user_lemmas_names = map #1 user_rules
    1.38 @@ -861,8 +856,6 @@
    1.39        val axcls_list = map (fn ngcls => get_relevant_clauses thy included_cls white_cls (map prop_of ngcls)) goal_cls
    1.40        val _ = app (fn axcls => Output.debug ("filtered clauses = " ^ Int.toString(length axcls)))
    1.41                    axcls_list
    1.42 -      val keep_types = if is_fol_logic logic then !ResClause.keep_types
    1.43 -                       else is_typed_hol ()
    1.44        val writer = if !prover = "spass" then dfg_writer else tptp_writer
    1.45        fun write_all [] [] _ = []
    1.46          | write_all (ccls::ccls_list) (axcls::axcls_list) k =
    1.47 @@ -875,12 +868,9 @@
    1.48                  and supers = tvar_classes_of_terms axtms
    1.49                  and tycons = type_consts_of_terms thy (ccltms@axtms)
    1.50                  (*TFrees in conjecture clauses; TVars in axiom clauses*)
    1.51 -                val classrel_clauses =
    1.52 -                      if keep_types then ResClause.make_classrel_clauses thy subs supers
    1.53 -                      else []
    1.54 +                val classrel_clauses = ResClause.make_classrel_clauses thy subs supers
    1.55                  val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
    1.56 -                val arity_clauses = if keep_types then ResClause.arity_clause_thy thy tycons supers
    1.57 -                                    else []
    1.58 +                val arity_clauses = ResClause.arity_clause_thy thy tycons supers
    1.59                  val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    1.60                  val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
    1.61                  val thm_names = Array.fromList clnames