# HG changeset patch
# User blanchet
# Date 1332856753 -10800
# Node ID ffc6d6267a880bd956e61531c006c6db397e24f4
# Parent  9bfc32fc7cedfadf4fb108b2f8b13a262ed94541
TFF: declare free types as types

diff -r 9bfc32fc7ced -r ffc6d6267a88 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 15:34:04 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
@@ -2035,14 +2035,21 @@
            |> close_formula_universally
            |> bound_tvars type_enc true atomic_types, NONE, [])
 
+fun type_enc_needs_free_types (Simple_Types (_, Polymorphic, _)) = true
+  | type_enc_needs_free_types (Simple_Types _) = false
+  | type_enc_needs_free_types _ = true
+
 fun formula_line_for_free_type j phi =
   Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
 fun formula_lines_for_free_types type_enc (facts : translated_formula list) =
-  let
-    val phis =
-      fold (union (op =)) (map #atomic_types facts) []
-      |> formulas_for_types type_enc add_sorts_on_tfree
-  in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
+  if type_enc_needs_free_types type_enc then
+    let
+      val phis =
+        fold (union (op =)) (map #atomic_types facts) []
+        |> formulas_for_types type_enc add_sorts_on_tfree
+    in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
+  else
+    []
 
 (** Symbol declarations **)
 
@@ -2497,8 +2504,11 @@
     val ind =
       case type_enc of
         Simple_Types _ =>
-        if String.isPrefix type_const_prefix s then atype_of_types
-        else individual_atype
+        if String.isPrefix type_const_prefix s orelse
+           String.isPrefix tfree_prefix s then
+          atype_of_types
+        else
+          individual_atype
       | _ => individual_atype
     fun typ 0 = if pred_sym then bool_atype else ind
       | typ ary = AFun (ind, typ (ary - 1))