src/HOL/Hoare/Arith2.thy

--- a/src/HOL/Hoare/Arith2.thy	Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Hoare/Arith2.thy	Fri Jul 24 13:03:20 1998 +0200
@@ -16,8 +16,9 @@
   "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
 
 consts fac     :: nat => nat
-primrec fac nat
-"fac 0 = Suc 0"
-"fac(Suc n) = (Suc n)*fac(n)"
+
+primrec
+  "fac 0 = Suc 0"
+  "fac(Suc n) = (Suc n)*fac(n)"
 
 end