src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42449 494e4ac5b0f8
parent 42361 23f352990944
child 42520 d1f7c4a01dbe
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Apr 21 21:14:06 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Apr 21 22:18:28 2011 +0200
     1.3 @@ -21,7 +21,8 @@
     1.4    val precise_overloaded_args : bool Unsynchronized.ref
     1.5    val fact_prefix : string
     1.6    val conjecture_prefix : string
     1.7 -  val types_dangerous_types : type_system -> bool
     1.8 +  val is_type_system_sound : type_system -> bool
     1.9 +  val type_system_types_dangerous_types : type_system -> bool
    1.10    val num_atp_type_args : theory -> type_system -> string -> int
    1.11    val translate_atp_fact :
    1.12      Proof.context -> bool -> (string * 'a) * thm
    1.13 @@ -67,8 +68,11 @@
    1.14    Mangled |
    1.15    No_Types
    1.16  
    1.17 -fun types_dangerous_types (Tags _) = true
    1.18 -  | types_dangerous_types _ = false
    1.19 +fun is_type_system_sound (Tags true) = true
    1.20 +  | is_type_system_sound _ = false
    1.21 +
    1.22 +fun type_system_types_dangerous_types (Tags _) = true
    1.23 +  | type_system_types_dangerous_types _ = false
    1.24  
    1.25  (* This is an approximation. If it returns "true" for a constant that isn't
    1.26     overloaded (i.e., that has one uniform definition), needless clutter is
    1.27 @@ -289,7 +293,7 @@
    1.28  
    1.29  fun get_helper_facts ctxt explicit_forall type_sys formulas =
    1.30    let
    1.31 -    val no_dangerous_types = types_dangerous_types type_sys
    1.32 +    val no_dangerous_types = type_system_types_dangerous_types type_sys
    1.33      val ct = init_counters |> fold count_formula formulas
    1.34      fun is_used s = the (Symtab.lookup ct s) > 0
    1.35      fun dub c needs_full_types (th, j) =