--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Dec 19 15:04:21 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Dec 19 15:47:17 2013 +0100
@@ -21,7 +21,7 @@
AAtom of 'c
datatype 'a atp_type =
- AType of 'a * 'a atp_type list |
+ AType of ('a * 'a list) * 'a atp_type list |
AFun of 'a atp_type * 'a atp_type |
APi of 'a list * 'a atp_type
@@ -165,7 +165,7 @@
AAtom of 'c
datatype 'a atp_type =
- AType of 'a * 'a atp_type list |
+ AType of ('a * 'a list) * 'a atp_type list |
AFun of 'a atp_type * 'a atp_type |
APi of 'a list * 'a atp_type
@@ -273,8 +273,8 @@
fun is_tptp_variable s = s <> "" andalso Char.isUpper (String.sub (s, 0))
val is_tptp_user_symbol = not o (is_tptp_variable orf is_built_in_tptp_symbol)
-val bool_atype = AType (`I tptp_bool_type, [])
-val individual_atype = AType (`I tptp_individual_type, [])
+val bool_atype = AType ((`I tptp_bool_type, []), [])
+val individual_atype = AType ((`I tptp_individual_type, []), [])
fun raw_polarities_of_conn ANot = (SOME false, NONE)
| raw_polarities_of_conn AAnd = (SOME true, SOME true)
@@ -324,8 +324,7 @@
fun strip_atype ty = ty |> strip_api ||> strip_afun
-fun is_function_atype ty =
- snd (snd (strip_atype ty)) <> AType (tptp_bool_type, [])
+fun is_function_atype ty = snd (snd (strip_atype ty)) <> AType ((tptp_bool_type, []), [])
fun is_predicate_atype ty = not (is_function_atype ty)
fun is_nontrivial_predicate_atype (AType _) = false
| is_nontrivial_predicate_atype ty = is_predicate_atype ty
@@ -356,9 +355,9 @@
fun uncurry_type (APi (tys, ty)) = APi (tys, uncurry_type ty)
| uncurry_type (ty as AFun (ty1 as AType _, ty2)) =
(case uncurry_type ty2 of
- AFun (ty' as AType (s, tys), ty) =>
- AFun (AType (tptp_product_type,
- ty1 :: (if s = tptp_product_type then tys else [ty'])), ty)
+ AFun (ty' as AType ((s, _), tys), ty) =>
+ AFun (AType ((tptp_product_type, []),
+ ty1 :: (if s = tptp_product_type then tys else [ty'])), ty)
| _ => ty)
| uncurry_type (ty as AType _) = ty
| uncurry_type _ =
@@ -372,9 +371,9 @@
fun str_of_type format ty =
let
val dfg = case format of DFG _ => true | _ => false
- fun str _ (AType (s, [])) =
+ fun str _ (AType ((s, _), [])) =
if dfg andalso s = tptp_individual_type then dfg_individual_type else s
- | str _ (AType (s, tys)) =
+ | str _ (AType ((s, _), tys)) =
let val ss = tys |> map (str false) in
if s = tptp_product_type then
ss |> space_implode
@@ -411,8 +410,7 @@
s ^
(if is_format_typed format then
" " ^ tptp_has_type ^ " " ^
- (ty |> the_default (AType (tptp_individual_type, []))
- |> string_of_type format)
+ (ty |> the_default (AType ((tptp_individual_type, []), [])) |> string_of_type format)
else
"")
@@ -507,7 +505,7 @@
| tptp_string_of_format (THF _) = tptp_thf
| tptp_string_of_format (DFG _) = raise Fail "non-TPTP format"
-val atype_of_types = AType (tptp_type_of_types, [])
+val atype_of_types = AType ((tptp_type_of_types, []), [])
fun nary_type_decl_type n = funpow n (curry AFun atype_of_types) atype_of_types
@@ -910,21 +908,22 @@
| DFG _ => avoid_clash_with_dfg_keywords
| _ => I
val nice_name = nice_name avoid_clash
+
fun nice_bound_tvars xs =
fold_map (nice_name o fst) xs
##>> fold_map (fold_map nice_name o snd) xs
#>> op ~~
- fun nice_type (AType (name, tys)) =
- nice_name name ##>> fold_map nice_type tys #>> AType
+
+ fun nice_type (AType ((name, clss), tys)) =
+ nice_name name ##>> fold_map nice_name clss ##>> fold_map nice_type tys #>> AType
| nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
- | nice_type (APi (names, ty)) =
- fold_map nice_name names ##>> nice_type ty #>> APi
+ | nice_type (APi (names, ty)) = fold_map nice_name names ##>> nice_type ty #>> APi
+
fun nice_term (ATerm ((name, tys), ts)) =
- nice_name name ##>> fold_map nice_type tys ##>> fold_map nice_term ts
- #>> ATerm
+ nice_name name ##>> fold_map nice_type tys ##>> fold_map nice_term ts #>> ATerm
| nice_term (AAbs (((name, ty), tm), args)) =
- nice_name name ##>> nice_type ty ##>> nice_term tm
- ##>> fold_map nice_term args #>> AAbs
+ nice_name name ##>> nice_type ty ##>> nice_term tm ##>> fold_map nice_term args #>> AAbs
+
fun nice_formula (ATyQuant (q, xs, phi)) =
fold_map (nice_type o fst) xs
##>> fold_map (fold_map nice_name o snd) xs
@@ -939,14 +938,14 @@
| nice_formula (AConn (c, phis)) =
fold_map nice_formula phis #>> curry AConn c
| nice_formula (AAtom tm) = nice_term tm #>> AAtom
+
fun nice_line (Class_Decl (ident, cl, cls)) =
nice_name cl ##>> fold_map nice_name cls
#>> (fn (cl, cls) => Class_Decl (ident, cl, cls))
| nice_line (Type_Decl (ident, ty, ary)) =
nice_name ty #>> (fn ty => Type_Decl (ident, ty, ary))
| nice_line (Sym_Decl (ident, sym, ty)) =
- nice_name sym ##>> nice_type ty
- #>> (fn (sym, ty) => Sym_Decl (ident, sym, ty))
+ nice_name sym ##>> nice_type ty #>> (fn (sym, ty) => Sym_Decl (ident, sym, ty))
| nice_line (Datatype_Decl (ident, xs, ty, tms)) =
nice_bound_tvars xs ##>> nice_type ty ##>> fold_map nice_term tms
#>> (fn ((xs, ty), tms) => Datatype_Decl (ident, xs, ty, tms))
@@ -954,11 +953,12 @@
nice_bound_tvars xs ##>> nice_type ty ##>> nice_name cl
#>> (fn ((xs, ty), cl) => Class_Memb (ident, xs, ty, cl))
| nice_line (Formula (ident, kind, phi, source, info)) =
- nice_formula phi
- #>> (fn phi => Formula (ident, kind, phi, source, info))
+ nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info))
+
fun nice_problem problem =
- fold_map (fn (heading, lines) =>
- fold_map nice_line lines #>> pair heading) problem
- in nice_problem problem empty_pool end
+ fold_map (fn (heading, lines) => fold_map nice_line lines #>> pair heading) problem
+ in
+ nice_problem problem empty_pool
+ end
end;
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Dec 19 15:04:21 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Dec 19 15:47:17 2013 +0100
@@ -439,8 +439,8 @@
val tvar_a_name = tvar_name tvar_a_z
val itself_name = `make_fixed_type_const @{type_name itself}
val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
-val tvar_a_atype = AType (tvar_a_name, [])
-val a_itself_atype = AType (itself_name, [tvar_a_atype])
+val tvar_a_atype = AType ((tvar_a_name, []), [])
+val a_itself_atype = AType ((itself_name, []), [tvar_a_atype])
(** Definitions and functions for FOL clauses and formulas for TPTP **)
@@ -479,8 +479,7 @@
| all_class_pairs thy tycons cls =
let
fun maybe_insert_class s =
- (s <> class_of_types andalso not (member (op =) cls s))
- ? insert (op =) s
+ (s <> class_of_types andalso not (member (op =) cls s)) ? insert (op =) s
val pairs = class_pairs thy tycons cls
val new_cls =
[] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) pairs
@@ -495,12 +494,10 @@
else if member (op =) seen cl then
(* multiple clauses for the same (tycon, cl) pair *)
make_axiom_tcon_clause (tcons,
- lookup_const tcons ^ "___" ^ ascii_of cl ^ "_" ^ string_of_int n,
- ar) ::
+ lookup_const tcons ^ "___" ^ ascii_of cl ^ "_" ^ string_of_int n, ar) ::
tcon_clause seen (n + 1) ((tcons, ars) :: rest)
else
- make_axiom_tcon_clause (tcons, lookup_const tcons ^ "___" ^ ascii_of cl,
- ar) ::
+ make_axiom_tcon_clause (tcons, lookup_const tcons ^ "___" ^ ascii_of cl, ar) ::
tcon_clause (cl :: seen) n ((tcons, ars) :: rest)
fun make_tcon_clauses thy tycons =
@@ -905,28 +902,26 @@
val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
val fused_infinite_type = Type (fused_infinite_type_name, [])
-fun raw_ho_type_of_typ type_enc =
+fun raw_atp_type_of_typ type_enc =
let
fun term (Type (s, Ts)) =
- AType (case (is_type_enc_higher_order type_enc, s) of
+ AType ((case (is_type_enc_higher_order type_enc, s) of
(true, @{type_name bool}) => `I tptp_bool_type
| (true, @{type_name fun}) => `I tptp_fun_type
- | _ => if s = fused_infinite_type_name andalso
- is_type_enc_native type_enc then
- `I tptp_individual_type
- else
- `make_fixed_type_const s,
- map term Ts)
- | term (TFree (s, _)) = AType (`make_tfree s, [])
- | term (TVar z) = AType (tvar_name z, [])
+ | _ =>
+ if s = fused_infinite_type_name andalso is_type_enc_native type_enc then
+ `I tptp_individual_type
+ else
+ `make_fixed_type_const s, []), map term Ts)
+ | term (TFree (s, _)) = AType ((`make_tfree s, []), [])
+ | term (TVar (z as (_, S))) = AType ((tvar_name z, []), [])
in term end
-fun atp_term_of_ho_type (AType (name, tys)) =
- ATerm ((name, []), map atp_term_of_ho_type tys)
- | atp_term_of_ho_type _ = raise Fail "unexpected type"
+fun atp_term_of_atp_type (AType ((name, _), tys)) = ATerm ((name, []), map atp_term_of_atp_type tys)
+ | atp_term_of_atp_type _ = raise Fail "unexpected type"
-fun ho_type_of_type_arg type_enc T =
- if T = dummyT then NONE else SOME (raw_ho_type_of_typ type_enc T)
+fun atp_type_of_type_arg type_enc T =
+ if T = dummyT then NONE else SOME (raw_atp_type_of_typ type_enc T)
(* This shouldn't clash with anything else. *)
val uncurried_alias_sep = "\000"
@@ -934,29 +929,23 @@
val ascii_of_uncurried_alias_sep = ascii_of uncurried_alias_sep
-fun generic_mangled_type_name f (AType (name, [])) = f name
- | generic_mangled_type_name f (AType (name, tys)) =
- f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
- ^ ")"
+fun generic_mangled_type_name f (AType ((name, _), [])) = f name
+ | generic_mangled_type_name f (AType ((name, _), tys)) =
+ f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys) ^ ")"
| generic_mangled_type_name _ _ = raise Fail "unexpected type"
-fun mangled_type type_enc =
- generic_mangled_type_name fst o raw_ho_type_of_typ type_enc
+fun mangled_type type_enc = generic_mangled_type_name fst o raw_atp_type_of_typ type_enc
fun make_native_type s =
- if s = tptp_bool_type orelse s = tptp_fun_type orelse
- s = tptp_individual_type then
- s
- else
- native_type_prefix ^ ascii_of s
+ if s = tptp_bool_type orelse s = tptp_fun_type orelse s = tptp_individual_type then s
+ else native_type_prefix ^ ascii_of s
-fun native_ho_type_of_raw_ho_type type_enc pred_sym ary =
+fun native_atp_type_of_raw_atp_type type_enc pred_sym ary =
let
fun to_mangled_atype ty =
- AType ((make_native_type (generic_mangled_type_name fst ty),
- generic_mangled_type_name snd ty), [])
- fun to_poly_atype (AType (name, tys)) =
- AType (name, map to_poly_atype tys)
+ AType (((make_native_type (generic_mangled_type_name fst ty),
+ generic_mangled_type_name snd ty), []), [])
+ fun to_poly_atype (AType ((name, clss), tys)) = AType ((name, clss), map to_poly_atype tys)
| to_poly_atype _ = raise Fail "unexpected type"
val to_atype =
if is_type_enc_polymorphic type_enc then to_poly_atype
@@ -965,14 +954,13 @@
fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
| to_fo ary (AType (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
| to_fo _ _ = raise Fail "unexpected type"
- fun to_ho (ty as AType ((s, _), tys)) =
+ fun to_ho (ty as AType (((s, _), _), tys)) =
if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
| to_ho _ = raise Fail "unexpected type"
in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
-fun native_ho_type_of_typ type_enc pred_sym ary =
- native_ho_type_of_raw_ho_type type_enc pred_sym ary
- o raw_ho_type_of_typ type_enc
+fun native_atp_type_of_typ type_enc pred_sym ary =
+ native_atp_type_of_raw_atp_type type_enc pred_sym ary o raw_atp_type_of_typ type_enc
(* Make atoms for sorted type variables. *)
fun generic_add_sorts_on_type _ [] = I
@@ -986,10 +974,9 @@
fun process_type_args type_enc T_args =
if is_type_enc_native type_enc then
- (map (native_ho_type_of_typ type_enc false 0) T_args, [])
+ (map (native_atp_type_of_typ type_enc false 0) T_args, [])
else
- ([], map_filter (Option.map atp_term_of_ho_type
- o ho_type_of_type_arg type_enc) T_args)
+ ([], map_filter (Option.map atp_term_of_atp_type o atp_type_of_type_arg type_enc) T_args)
fun class_atom type_enc (cl, T) =
let
@@ -998,9 +985,9 @@
val tm_args =
tm_args @
(case type_enc of
- Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
- [ATerm ((TYPE_name, ty_args), [])]
- | _ => [])
+ Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
+ [ATerm ((TYPE_name, ty_args), [])]
+ | _ => [])
in AAtom (ATerm ((cl, ty_args), tm_args)) end
fun class_atoms type_enc (cls, T) =
@@ -1070,7 +1057,7 @@
ty_args ""
in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
fun mangled_const_name type_enc =
- map_filter (ho_type_of_type_arg type_enc)
+ map_filter (atp_type_of_type_arg type_enc)
#> raw_mangled_const_name generic_mangled_type_name
val parse_mangled_ident =
@@ -1788,11 +1775,9 @@
#> (case type_enc of
Native (_, poly, _) =>
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)
+ (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)))
fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
@@ -2065,11 +2050,10 @@
end
fun do_bound_type ctxt mono type_enc =
- case type_enc of
+ (case type_enc of
Native (_, _, level) =>
- fused_type ctxt mono level 0 #> native_ho_type_of_typ type_enc false 0
- #> SOME
- | _ => K NONE
+ fused_type ctxt mono level 0 #> native_atp_type_of_typ type_enc false 0 #> SOME
+ | _ => K NONE)
fun tag_with_type ctxt mono type_enc pos T tm =
IConst (type_tag, T --> T, [T])
@@ -2103,7 +2087,7 @@
map (term Elsewhere) args |> mk_aterm type_enc name []
| IAbs ((name, T), tm) =>
if is_type_enc_higher_order type_enc then
- AAbs (((name, native_ho_type_of_typ type_enc true 0 T), (* FIXME? why "true"? *)
+ AAbs (((name, native_atp_type_of_typ type_enc true 0 T), (* FIXME? why "true"? *)
term Elsewhere tm), map (term Elsewhere) args)
else
raise Fail "unexpected lambda-abstraction"
@@ -2130,8 +2114,7 @@
else
NONE
fun do_formula pos (ATyQuant (q, xs, phi)) =
- ATyQuant (q, map (apfst (native_ho_type_of_typ type_enc false 0)) xs,
- do_formula pos phi)
+ ATyQuant (q, map (apfst (native_atp_type_of_typ type_enc false 0)) xs, do_formula pos phi)
| do_formula pos (AQuant (q, xs, phi)) =
let
val phi = phi |> do_formula pos
@@ -2193,10 +2176,8 @@
fun line_of_tcon_clause type_enc (name, prems, (cl, T)) =
if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
Class_Memb (class_memb_prefix ^ name,
- map (fn (cls, T) =>
- (T |> dest_TVar |> tvar_name, map (`make_class) cls))
- prems,
- native_ho_type_of_typ type_enc false 0 T, `make_class cl)
+ map (fn (cls, T) => (T |> dest_TVar |> tvar_name, map (`make_class) cls)) prems,
+ native_atp_type_of_typ type_enc false 0 T, `make_class cl)
else
Formula ((tcon_clause_prefix ^ name, ""), Axiom,
mk_ahorn (maps (class_atoms type_enc) prems)
@@ -2220,10 +2201,10 @@
fun line j (cl, T) =
if type_classes then
Class_Memb (class_memb_prefix ^ string_of_int j, [],
- native_ho_type_of_typ type_enc false 0 T, `make_class cl)
+ native_atp_type_of_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, [])
+ class_atom type_enc (cl, T), NONE, [])
val membs =
fold (union (op =)) (map #atomic_types facts) []
|> class_membs_of_types type_enc add_sorts_on_tfree
@@ -2430,7 +2411,7 @@
in
Sym_Decl (sym_decl_prefix ^ s, (s, s'),
T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
- |> native_ho_type_of_typ type_enc pred_sym ary
+ |> native_atp_type_of_typ type_enc pred_sym ary
|> not (null T_args)
? curry APi (map (tvar_name o dest_TVar) T_args))
end
@@ -2572,7 +2553,7 @@
fun datatype_of_ctrs (ctrs as (_, T1) :: _) =
let val ctrs' = map do_ctr ctrs in
if forall is_some ctrs' then
- SOME (native_ho_type_of_typ type_enc false 0 (body_type T1), map_filter I ctrs')
+ SOME (native_atp_type_of_typ type_enc false 0 (body_type T1), map_filter I ctrs')
else
NONE
end
@@ -2583,8 +2564,8 @@
[]
| datatypes_of_sym_table _ _ _ _ _ _ = []
-fun decl_line_of_datatype (ty as AType ((_, s'), ty_args), ctrs) =
- let val xs = map (fn AType (name, []) => name) ty_args in
+fun decl_line_of_datatype (ty as AType (((_, s'), _), ty_args), ctrs) =
+ let val xs = map (fn AType ((name, _), []) => name) ty_args in
Datatype_Decl (datatype_decl_prefix ^ ascii_of s', map (rpair []) xs, ty, ctrs)
end
@@ -2685,7 +2666,7 @@
if is_tptp_user_symbol s then Symtab.default (s, (name, value)) else I
fun do_class name = apfst (apfst (do_sym name ()))
val do_bound_tvars = fold do_class o snd
- fun do_type (AType (name, tys)) =
+ fun do_type (AType ((name, _), tys)) =
apfst (apsnd (do_sym name (length tys))) #> fold do_type tys
| do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
| do_type (APi (_, ty)) = do_type ty
--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Dec 19 15:04:21 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Dec 19 15:47:17 2013 +0100
@@ -258,11 +258,11 @@
fun list_app (f, args) = fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f
-fun parse_sort x = scan_general_id x
-and parse_sorts x = (parse_sort ::: Scan.repeat ($$ "&" |-- parse_sort)) x
+fun parse_class x = scan_general_id x
+and parse_classes x = (parse_class ::: Scan.repeat ($$ "&" |-- parse_class)) x
fun parse_type x =
- (scan_general_id --| Scan.option ($$ "{" |-- parse_sorts --| $$ "}")
+ (scan_general_id -- Scan.optional ($$ "{" |-- parse_classes --| $$ "}") []
-- Scan.optional ($$ "(" |-- parse_types --| $$ ")") []
>> AType) x
and parse_types x = (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x
@@ -530,7 +530,7 @@
fun map_term_names_in_atp_proof f =
let
- fun map_type (AType (s, tys)) = AType (f s, map map_type tys)
+ fun map_type (AType ((s, clss), tys)) = AType ((f s, map f clss), map map_type tys)
| map_type (AFun (ty, ty')) = AFun (map_type ty, map_type ty')
| map_type (APi (ss, ty)) = APi (map f ss, map_type ty)
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Dec 19 15:04:21 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Dec 19 15:47:17 2013 +0100
@@ -108,15 +108,21 @@
TFree (ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))
end
+exception ATP_CLASS of string list
exception ATP_TYPE of string atp_type list
exception ATP_TERM of (string, string atp_type) atp_term list
exception ATP_FORMULA of
(string, string, (string, string atp_type) atp_term, string) atp_formula list
exception SAME of unit
+fun class_of_atp_class cls =
+ (case unprefix_and_unascii class_prefix cls of
+ SOME s => s
+ | NONE => raise ATP_CLASS [cls])
+
(* Type variables are given the basic sort "HOL.type". Some will later be constrained by information
from type literals, or by type inference. *)
-fun typ_of_atp_type ctxt (ty as AType (a, tys)) =
+fun typ_of_atp_type ctxt (ty as AType ((a, clss), tys)) =
let val Ts = map (typ_of_atp_type ctxt) tys in
(case unprefix_and_unascii type_const_prefix a of
SOME b => Type (invert_const b, Ts)
@@ -130,10 +136,12 @@
(* The term could be an Isabelle variable or a variable from the ATP, say "X1" or "_5018".
Sometimes variables from the ATP are indistinguishable from Isabelle variables, which
forces us to use a type parameter in all cases. *)
- Type_Infer.param 0 (a |> perhaps (unprefix_and_unascii tvar_prefix), HOLogic.typeS)))
+ Type_Infer.param 0 (a |> perhaps (unprefix_and_unascii tvar_prefix),
+ (if null clss then HOLogic.typeS
+ else map class_of_atp_class clss))))
end
-fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType (s, map atp_type_of_atp_term us)
+fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType ((s, []), map atp_type_of_atp_term us)
fun typ_of_atp_term ctxt = typ_of_atp_type ctxt o atp_type_of_atp_term