equal
deleted
inserted
replaced
231 |
231 |
232 val forbidden_thms = |
232 val forbidden_thms = |
233 ["finite_intvl_succ_class", |
233 ["finite_intvl_succ_class", |
234 "nibble"] |
234 "nibble"] |
235 |
235 |
236 val forbidden_consts = |
236 val forbidden_consts = [@{const_name Pure.type}] |
237 [@{const_name Pure.type}, @{const_name Datatype.dsum}, @{const_name Datatype.usum}] |
|
238 |
237 |
239 fun is_forbidden_theorem (s, th) = |
238 fun is_forbidden_theorem (s, th) = |
240 let val consts = Term.add_const_names (prop_of th) [] in |
239 let val consts = Term.add_const_names (prop_of th) [] in |
241 exists (member (op =) (Long_Name.explode s)) forbidden_thms orelse |
240 exists (member (op =) (Long_Name.explode s)) forbidden_thms orelse |
242 exists (member (op =) forbidden_consts) consts orelse |
241 exists (member (op =) forbidden_consts) consts orelse |