# HG changeset patch
# User bulwahn
# Date 1328460194 -3600
# Node ID b67bb064de1e9e6561536cb7ad7077020a688b17
# Parent  ce8f7944fd6b45f1b744f70af754820d75ee3594
mutabelle ignores theorems with internal constants

diff -r ce8f7944fd6b -r b67bb064de1e src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Feb 05 17:09:21 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Feb 05 17:43:14 2012 +0100
@@ -241,7 +241,8 @@
   "nibble"]
 
 val forbidden_consts =
- [@{const_name nibble_pair_of_char}, @{const_name "TYPE"}]
+ [@{const_name nibble_pair_of_char}, @{const_name "TYPE"},
+  @{const_name Datatype.dsum}, @{const_name Datatype.usum}]
 
 fun is_forbidden_theorem (s, th) =
   let val consts = Term.add_const_names (prop_of th) [] in