# HG changeset patch # User haftmann # Date 1153632082 -7200 # Node ID 56207a6f4cc5831e15c4381633c8793ff4a90e5f # Parent 183f08468e192c3fed24745d97d1d205affc25ce fixed bug for serialization for uminus on ints diff -r 183f08468e19 -r 56207a6f4cc5 src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Sun Jul 23 07:20:52 2006 +0200 +++ b/src/HOL/Integ/IntDef.thy Sun Jul 23 07:21:22 2006 +0200 @@ -914,7 +914,7 @@ ml ("IntInf.* (_, _)") haskell (infixl 7 "*") "uminus :: int \ int" - ml (target_atom "~") + ml (target_atom "IntInf.~") haskell (target_atom "negate") "op = :: int \ int \ bool" ml ("(op =) (_ : IntInf.int, _)")