src/HOL/Mutabelle/mutabelle_extra.ML
changeset 38864 4abe644fcea5
parent 38857 97775f3e8722
child 39133 70d3915c92f0
     1.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -187,7 +187,7 @@
     1.4  val nitpick_mtd = ("nitpick", invoke_nitpick)
     1.5  *)
     1.6  
     1.7 -val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}]
     1.8 +val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]
     1.9  
    1.10  val forbidden =
    1.11   [(* (@{const_name "power"}, "'a"), *)