# HG changeset patch # User haftmann # Date 1166426488 -3600 # Node ID 75ba582dd6e9a6ea47d8c7a2c2d8e825731dc46d # Parent 9ce66839d9f1784f1c550fdd740592a33742a3da whitespace fix diff -r 9ce66839d9f1 -r 75ba582dd6e9 src/HOL/Integ/IntArith.thy --- a/src/HOL/Integ/IntArith.thy Mon Dec 18 08:21:27 2006 +0100 +++ b/src/HOL/Integ/IntArith.thy Mon Dec 18 08:21:28 2006 +0100 @@ -407,7 +407,7 @@ (SML "_" and "0/ :/ IntInf.int" and "~1/ :/ IntInf.int" - and "(_; _; raise FAIL \"BIT\")" + and "(_; _; raise Fail \"BIT\")" and "IntInf.+/ (_,/ 1)" and "IntInf.-/ (_,/ 1))") (Haskell "_"