src/HOL/Tools/ATP/atp_translate.ML
changeset 43192 9c29a00f2970
parent 43189 0ab7265f659f
child 43193 e11bd628f1a5
equal deleted inserted replaced
43191:0a72c0527111 43192:9c29a00f2970
  1397       |> map_filter (fn (NONE, _) => NONE
  1397       |> map_filter (fn (NONE, _) => NONE
  1398                       | (SOME fact, (name, _)) => SOME (fact, name))
  1398                       | (SOME fact, (name, _)) => SOME (fact, name))
  1399       |> ListPair.unzip
  1399       |> ListPair.unzip
  1400     (* Remove existing facts from the conjecture, as this can dramatically
  1400     (* Remove existing facts from the conjecture, as this can dramatically
  1401        boost an ATP's performance (for some reason). *)
  1401        boost an ATP's performance (for some reason). *)
  1402     val hyp_ts = hyp_ts |> filter_out (member (op aconv) fact_ts)
  1402     val hyp_ts =
       
  1403       hyp_ts
       
  1404       |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
  1403     val goal_t = Logic.list_implies (hyp_ts, concl_t)
  1405     val goal_t = Logic.list_implies (hyp_ts, concl_t)
  1404     val all_ts = goal_t :: fact_ts
  1406     val all_ts = goal_t :: fact_ts
  1405     val subs = tfree_classes_of_terms all_ts
  1407     val subs = tfree_classes_of_terms all_ts
  1406     val supers = tvar_classes_of_terms all_ts
  1408     val supers = tvar_classes_of_terms all_ts
  1407     val tycons = type_constrs_of_terms thy all_ts
  1409     val tycons = type_constrs_of_terms thy all_ts