src/HOL/Mutabelle/mutabelle_extra.ML
changeset 59940 087d81f5213e
parent 59621 291934bac95e
child 59970 e9f73d87d904
     1.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Apr 06 22:11:01 2015 +0200
     1.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Apr 06 23:14:05 2015 +0200
     1.3 @@ -247,10 +247,10 @@
     1.4    end
     1.5  
     1.6  val forbidden_mutant_constnames =
     1.7 - ["HOL.induct_equal",
     1.8 -  "HOL.induct_implies",
     1.9 -  "HOL.induct_conj",
    1.10 -  "HOL.induct_forall",
    1.11 +[@{const_name HOL.induct_equal},
    1.12 + @{const_name HOL.induct_implies},
    1.13 + @{const_name HOL.induct_conj},
    1.14 + @{const_name HOL.induct_forall},
    1.15   @{const_name undefined},
    1.16   @{const_name default},
    1.17   @{const_name Pure.dummy_pattern},