src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 41384 c4488b7cbe3b
parent 41313 a96ac4d180b7
child 41406 062490d081b9
equal deleted inserted replaced
41374:a35af5180c01 41384:c4488b7cbe3b
   652 val fact_max_weight = 1.0
   652 val fact_max_weight = 1.0
   653 
   653 
   654 fun add_term_weights weight (ATerm (s, tms)) =
   654 fun add_term_weights weight (ATerm (s, tms)) =
   655   (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
   655   (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
   656   #> fold (add_term_weights weight) tms
   656   #> fold (add_term_weights weight) tms
   657 val add_formula_weights = fold_formula o add_term_weights
       
   658 fun add_problem_line_weights weight (Fof (_, _, phi)) =
   657 fun add_problem_line_weights weight (Fof (_, _, phi)) =
   659   add_formula_weights weight phi
   658   fold_formula (add_term_weights weight) phi
   660 
   659 
   661 fun add_conjectures_weights [] = I
   660 fun add_conjectures_weights [] = I
   662   | add_conjectures_weights conjs =
   661   | add_conjectures_weights conjs =
   663     let val (hyps, conj) = split_last conjs in
   662     let val (hyps, conj) = split_last conjs in
   664       add_problem_line_weights conj_weight conj
   663       add_problem_line_weights conj_weight conj