# HG changeset patch
# User blanchet
# Date 1327607394 -3600
# Node ID b02ff6b17599a8070b767593d215c5f30a16dcfd
# Parent  54227223a8d481aef76c8ab1e6173d360593b7df
better handling of individual type for DFG format (SPASS)

diff -r 54227223a8d4 -r b02ff6b17599 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Jan 26 12:04:05 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Jan 26 20:49:54 2012 +0100
@@ -283,11 +283,13 @@
   | flatten_type _ =
     raise Fail "unexpected higher-order type in first-order format"
 
+val dfg_individual_type = "i" (* shouldn't clash *)
+
 fun str_for_type format ty =
   let
     val dfg = (format = DFG DFG_Sorted)
     fun str _ (AType (s, [])) =
-        if dfg andalso s = tptp_individual_type then "Top" else s
+        if dfg andalso s = tptp_individual_type then dfg_individual_type else s
       | str _ (AType (s, tys)) =
         let val ss = tys |> map (str false) in
           if s = tptp_product_type then
@@ -488,7 +490,7 @@
     fun sorts () =
       filt (fn Decl (_, sym, AType (s, [])) =>
                if s = tptp_type_of_types then SOME sym else NONE
-             | _ => NONE)
+             | _ => NONE) @ [dfg_individual_type]
       |> commas |> enclose "sorts [" "]."
     val syms = [func_aries, pred_aries] @ (if sorted then [sorts ()] else [])
     fun func_sigs () =
diff -r 54227223a8d4 -r b02ff6b17599 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jan 26 12:04:05 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jan 26 20:49:54 2012 +0100
@@ -837,7 +837,7 @@
   | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
 fun close_iformula_universally phi = close_universally add_iterm_vars phi
 
-val fused_infinite_type_name = @{type_name ind} (* any infinite type *)
+val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
 val fused_infinite_type = Type (fused_infinite_type_name, [])
 
 fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)