# HG changeset patch
# User blanchet
# Date 1368709408 -7200
# Node ID dfa06e82a720c858945cfe8b340dfcf26cb7a5d4
# Parent  11b48e7a4e7e079306efbf133f39dc8f1d572bbd
tuned comments

diff -r 11b48e7a4e7e -r dfa06e82a720 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 16 14:58:30 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 16 15:03:28 2013 +0200
@@ -2182,7 +2182,6 @@
 
 fun line_of_tcon_clause type_enc (name, prems, (cl, T)) =
   if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
-    (* ### FIXME: is the list of type variables exhaustive? *)
     Class_Memb (class_memb_prefix ^ name,
                 map (fn (cls, T) =>
                         (T |> dest_TVar |> tvar_name, map (`make_class) cls))
@@ -2561,10 +2560,7 @@
   | datatypes_of_sym_table _ _ _ _ _ = []
 
 fun decl_line_of_datatype (ty as AType ((_, s'), ty_args), ctrs, exhaust) =
-  let
-    (* ### FIXME: Test datatypes with sort constraints *)
-    val xs = map (fn AType (name, []) => name) ty_args
-  in
+  let val xs = map (fn AType (name, []) => name) ty_args in
     Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty,
                    ctrs, exhaust)
   end