equal
deleted
inserted
replaced
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 = |
237 [@{const_name "TYPE"}, @{const_name Datatype.dsum}, @{const_name Datatype.usum}] |
237 [@{const_name Pure.type}, @{const_name Datatype.dsum}, @{const_name Datatype.usum}] |
238 |
238 |
239 fun is_forbidden_theorem (s, th) = |
239 fun is_forbidden_theorem (s, th) = |
240 let val consts = Term.add_const_names (prop_of th) [] in |
240 let val consts = Term.add_const_names (prop_of th) [] in |
241 exists (member (op =) (Long_Name.explode s)) forbidden_thms orelse |
241 exists (member (op =) (Long_Name.explode s)) forbidden_thms orelse |
242 exists (member (op =) forbidden_consts) consts orelse |
242 exists (member (op =) forbidden_consts) consts orelse |