src/HOL/Tools/ATP/atp_translate.ML
changeset 45829 0b19934792d2
parent 45828 3b8606fba2dd
child 45830 45a5b6edd4f7
equal deleted inserted replaced
45828:3b8606fba2dd 45829:0b19934792d2
  2020   in
  2020   in
  2021     Symtab.empty
  2021     Symtab.empty
  2022     |> is_type_enc_fairly_sound type_enc
  2022     |> is_type_enc_fairly_sound type_enc
  2023        ? (fold (fold add_fact_syms) [conjs, facts]
  2023        ? (fold (fold add_fact_syms) [conjs, facts]
  2024           #> (case type_enc of
  2024           #> (case type_enc of
  2025                 Simple_Types (First_Order, Polymorphic, _) => add_TYPE_const ()
  2025                 Simple_Types (First_Order, Polymorphic, _) =>
       
  2026                 if avoid_first_order_ghost_type_vars then add_TYPE_const ()
       
  2027                 else I
  2026               | Simple_Types _ => I
  2028               | Simple_Types _ => I
  2027               | _ => fold add_undefined_const (var_types ())))
  2029               | _ => fold add_undefined_const (var_types ())))
  2028   end
  2030   end
  2029 
  2031 
  2030 (* We add "bool" in case the helper "True_or_False" is included later. *)
  2032 (* We add "bool" in case the helper "True_or_False" is included later. *)