equal
deleted
inserted
replaced
87 Symtab.map_default (c, [ctyps]) |
87 Symtab.map_default (c, [ctyps]) |
88 (fn [] => [] | ctypss => insert (op =) ctyps ctypss) |
88 (fn [] => [] | ctypss => insert (op =) ctyps ctypss) |
89 |
89 |
90 val fresh_prefix = "Sledgehammer.Fresh." |
90 val fresh_prefix = "Sledgehammer.Fresh." |
91 val flip = Option.map not |
91 val flip = Option.map not |
92 val boring_natural_consts = [@{const_name If}] |
92 (* These are typically simplified away by "Meson.presimplify". *) |
|
93 val boring_consts = [@{const_name If}, @{const_name Let}] |
93 |
94 |
94 fun get_consts_typs thy pos ts = |
95 fun get_consts_typs thy pos ts = |
95 let |
96 let |
96 (* Free variables are included, as well as constants, to handle locales. |
97 (* Free variables are included, as well as constants, to handle locales. |
97 "skolem_id" is included to increase the complexity of theorems containing |
98 "skolem_id" is included to increase the complexity of theorems containing |
137 do_equality T t1 t2 |
138 do_equality T t1 t2 |
138 | (t0 as Const (_, @{typ bool})) $ t1 => |
139 | (t0 as Const (_, @{typ bool})) $ t1 => |
139 do_term t0 #> do_formula pos t1 (* theory constant *) |
140 do_term t0 #> do_formula pos t1 (* theory constant *) |
140 | _ => do_term t |
141 | _ => do_term t |
141 in |
142 in |
142 Symtab.empty |> fold (Symtab.update o rpair []) boring_natural_consts |
143 Symtab.empty |> fold (Symtab.update o rpair []) boring_consts |
143 |> fold (do_formula pos) ts |
144 |> fold (do_formula pos) ts |
144 end |
145 end |
145 |
146 |
146 (*Inserts a dummy "constant" referring to the theory name, so that relevance |
147 (*Inserts a dummy "constant" referring to the theory name, so that relevance |
147 takes the given theory into account.*) |
148 takes the given theory into account.*) |