--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200
@@ -494,6 +494,8 @@
fun dfg_string_for_formula poly gen_simp info =
let
val str_for_typ = string_for_type (DFG poly)
+ fun str_for_bound_typ (ty, []) = str_for_typ ty
+ | str_for_bound_typ (ty, sorts) = str_for_typ ty ^ " : " ^ commas sorts
fun suffix_tag top_level s =
if top_level then
case extract_isabelle_status info of
@@ -521,7 +523,7 @@
| str_for_conn _ AImplies = "implies"
| str_for_conn top_level AIff = "equiv" |> suffix_tag top_level
fun str_for_formula top_level (ATyQuant (q, xs, phi)) =
- str_for_quant q ^ "_sorts([" ^ commas (map (str_for_typ o fst) xs) ^
+ str_for_quant q ^ "_sorts([" ^ commas (map str_for_bound_typ xs) ^
"], " ^ str_for_formula top_level phi ^ ")"
| str_for_formula top_level (AQuant (q, xs, phi)) =
str_for_quant q ^ "([" ^
@@ -546,7 +548,6 @@
fun fun_typ sym ty = "function(" ^ sym ^ ", " ^ str_for_typ ty ^ ")."
fun pred_typ sym ty =
let
- val ((ty_vars, tys), _) = strip_atype ty
val (ty_vars, tys) =
strip_atype ty |> fst
|>> (fn [] => [] | ty_vars => ["[" ^ commas ty_vars ^ "]"])
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200
@@ -1739,12 +1739,17 @@
case filter is_TVar Ts of
[] => I
| Ts =>
- (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
- #> (if is_type_enc_native type_enc then
- mk_atyquant AForall
- (map (fn TVar (x, S) =>
- (AType (tvar_name x, []), map (`make_type_class) S)) Ts)
- else
+ ((sorts andalso polymorphism_of_type_enc type_enc <> Type_Class_Polymorphic)
+ ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
+ #> (case type_enc of
+ Native (_, poly, _) =>
+ mk_atyquant AForall (map (fn TVar (x, S) =>
+ (AType (tvar_name x, []),
+ if poly = Type_Class_Polymorphic then
+ map (`make_type_class) S
+ else
+ [])) Ts)
+ | _ =>
mk_aquant AForall (map (fn TVar (x, _) => (tvar_name x, NONE)) Ts))
fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =