| changeset 58111 | 82db9ad610b9 |
| parent 56467 | 8d7d6f17c6a7 |
| child 58843 | 521cea5fa777 |
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Sep 01 16:17:46 2014 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Sep 01 16:17:46 2014 +0200 @@ -233,8 +233,7 @@ ["finite_intvl_succ_class", "nibble"] -val forbidden_consts = - [@{const_name Pure.type}, @{const_name Datatype.dsum}, @{const_name Datatype.usum}] +val forbidden_consts = [@{const_name Pure.type}] fun is_forbidden_theorem (s, th) = let val consts = Term.add_const_names (prop_of th) [] in