366 higher-order places) but not by the monomorphizer. *) |
366 higher-order places) but not by the monomorphizer. *) |
367 [@{const_name all}, @{const_name "==>"}, @{const_name "=="}, |
367 [@{const_name all}, @{const_name "==>"}, @{const_name "=="}, |
368 @{const_name Trueprop}, @{const_name All}, @{const_name Ex}, |
368 @{const_name Trueprop}, @{const_name All}, @{const_name Ex}, |
369 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}] |
369 @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}] |
370 |
370 |
371 val atp_schematic_consts_of = |
371 fun add_schematic_const (x as (_, T)) = |
372 Monomorph.all_schematic_consts_of |
372 Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x |
373 #> Symtab.map (fn s => fn Ts => |
373 val add_schematic_consts_of = |
374 if member (op =) atp_monomorph_bad_consts s then [] else Ts) |
374 Term.fold_aterms (fn Const (x as (s, _)) => |
|
375 not (member (op =) atp_monomorph_bad_consts s) |
|
376 ? add_schematic_const x |
|
377 | _ => I) |
|
378 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty |
375 |
379 |
376 (** Definitions and functions for FOL clauses and formulas for TPTP **) |
380 (** Definitions and functions for FOL clauses and formulas for TPTP **) |
377 |
381 |
378 (* The first component is the type class; the second is a "TVar" or "TFree". *) |
382 (* The first component is the type class; the second is a "TVar" or "TFree". *) |
379 datatype type_literal = |
383 datatype type_literal = |