# HG changeset patch
# User blanchet
# Date 1454348718 -3600
# Node ID 42202671777c3f1153218079e025e10c1fba1dd0
# Parent  527488dc8b902a9bb0b56247740dc19bd3a57e43
avoid generating polymorphic SPASS constructs to monomorphic SPASS

diff -r 527488dc8b90 -r 42202671777c src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Jan 22 16:00:03 2016 +0000
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Feb 01 18:45:18 2016 +0100
@@ -1675,12 +1675,12 @@
        |> class_membs_of_types type_enc add_sorts_on_tvar
        |> map (class_atom type_enc)))
     #> (case type_enc of
-         Native (_, poly, _) =>
+         Native (_, Type_Class_Polymorphic, _) =>
          mk_atyquant AForall (map (fn TVar (z as (_, S)) =>
-           (AType ((tvar_name z, []), []),
-            if poly = Type_Class_Polymorphic then map (`make_class) (normalize_classes S)
-            else [])) Ts)
-        | _ => mk_aquant AForall (map (fn TVar z => (tvar_name z, NONE)) Ts)))
+           (AType ((tvar_name z, []), []), map (`make_class) (normalize_classes S) )) Ts)
+       | Native (_, Raw_Polymorphic _, _) =>
+         mk_atyquant AForall (map (fn TVar (z as (_, S)) => (AType ((tvar_name z, []), []), [])) Ts)
+       | _ => mk_aquant AForall (map (fn TVar z => (tvar_name z, NONE)) Ts)))
 
 fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
   (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])