author blanchet Tue Mar 27 16:59:13 2012 +0300 (2012-03-27) changeset 47145 ffc6d6267a88 parent 47144 9bfc32fc7ced child 47146 7276f2b12ff7
TFF: declare free types as types
```     1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 15:34:04 2012 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
1.3 @@ -2035,14 +2035,21 @@
1.4             |> close_formula_universally
1.5             |> bound_tvars type_enc true atomic_types, NONE, [])
1.6
1.7 +fun type_enc_needs_free_types (Simple_Types (_, Polymorphic, _)) = true
1.8 +  | type_enc_needs_free_types (Simple_Types _) = false
1.9 +  | type_enc_needs_free_types _ = true
1.10 +
1.11  fun formula_line_for_free_type j phi =
1.12    Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
1.13  fun formula_lines_for_free_types type_enc (facts : translated_formula list) =
1.14 -  let
1.15 -    val phis =
1.16 -      fold (union (op =)) (map #atomic_types facts) []
1.17 -      |> formulas_for_types type_enc add_sorts_on_tfree
1.18 -  in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
1.19 +  if type_enc_needs_free_types type_enc then
1.20 +    let
1.21 +      val phis =
1.22 +        fold (union (op =)) (map #atomic_types facts) []
1.23 +        |> formulas_for_types type_enc add_sorts_on_tfree
1.24 +    in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
1.25 +  else
1.26 +    []
1.27
1.28  (** Symbol declarations **)
1.29
1.30 @@ -2497,8 +2504,11 @@
1.31      val ind =
1.32        case type_enc of
1.33          Simple_Types _ =>
1.34 -        if String.isPrefix type_const_prefix s then atype_of_types
1.35 -        else individual_atype
1.36 +        if String.isPrefix type_const_prefix s orelse
1.37 +           String.isPrefix tfree_prefix s then
1.38 +          atype_of_types
1.39 +        else
1.40 +          individual_atype
1.41        | _ => individual_atype
1.42      fun typ 0 = if pred_sym then bool_atype else ind
1.43        | typ ary = AFun (ind, typ (ary - 1))
```