changeset 35671 | ed2c3830d881 |
parent 35665 | ff2bf50505ab |
child 35695 | 80b2c22f8f00 |
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Mar 09 09:25:23 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Mar 09 14:18:21 2010 +0100 @@ -1388,7 +1388,7 @@ (Func (R1, Formula Neut)) r)) (to_opt R1 u1) | _ => raise NUT ("Nitpick_Kodkod.to_r (SingletonSet)", [u])) - | Op1 (Tha, _, R, u1) => + | Op1 (SafeThe, _, R, u1) => if is_opt_rep R then kk_join (to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1) true_atom else