# HG changeset patch
# User blanchet
# Date 1341400124 -7200
# Node ID 086d9bb80d465318caa752cd24465a8cdf4e89d8
# Parent  7c48419c89c5b59b408c96e23b8bf3c45695d459
don't generate any type class axioms for free types for monomorphic encodings

diff -r 7c48419c89c5 -r 086d9bb80d46 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 04 13:08:44 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 04 13:08:44 2012 +0200
@@ -2184,19 +2184,24 @@
            |> bound_tvars type_enc true atomic_types, NONE, [])
 
 fun lines_for_free_types type_enc (facts : ifact list) =
-  let
-    fun line j (cl, T) =
-      if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
-        Class_Memb (class_memb_prefix ^ string_of_int j, [],
-                    native_ho_type_from_typ type_enc false 0 T,
-                    `make_class cl)
-      else
-        Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
-                 class_atom type_enc (cl, T), NONE, [])
-    val membs =
-      fold (union (op =)) (map #atomic_types facts) []
-      |> class_membs_for_types type_enc add_sorts_on_tfree
-  in map2 line (0 upto length membs - 1) membs end
+  if is_type_enc_polymorphic type_enc then
+    let
+      val type_classes =
+        (polymorphism_of_type_enc type_enc = Type_Class_Polymorphic)
+      fun line j (cl, T) =
+        if type_classes then
+          Class_Memb (class_memb_prefix ^ string_of_int j, [],
+                      native_ho_type_from_typ type_enc false 0 T,
+                      `make_class cl)
+        else
+          Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
+                   class_atom type_enc (cl, T), NONE, [])
+      val membs =
+        fold (union (op =)) (map #atomic_types facts) []
+        |> class_membs_for_types type_enc add_sorts_on_tfree
+    in map2 line (0 upto length membs - 1) membs end
+  else
+    []
 
 (** Symbol declarations **)