equal
deleted
inserted
replaced
427 |
427 |
428 fun add_schematic_const (x as (_, T)) = |
428 fun add_schematic_const (x as (_, T)) = |
429 Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x |
429 Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x |
430 val add_schematic_consts_of = |
430 val add_schematic_consts_of = |
431 Term.fold_aterms (fn Const (x as (s, _)) => |
431 Term.fold_aterms (fn Const (x as (s, _)) => |
432 not (member (op =) atp_widely_irrelevant_consts s) |
432 not (is_widely_irrelevant_const s) ? add_schematic_const x |
433 ? add_schematic_const x |
|
434 | _ => I) |
433 | _ => I) |
435 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty |
434 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty |
436 |
435 |
437 val tvar_a_str = "'a" |
436 val tvar_a_str = "'a" |
438 val tvar_a_z = ((tvar_a_str, 0), \<^sort>\<open>type\<close>) |
437 val tvar_a_z = ((tvar_a_str, 0), \<^sort>\<open>type\<close>) |