--- a/src/FOL/ex/Nat.thy Mon Feb 10 14:33:47 2014 +0100 +++ b/src/FOL/ex/Nat.thy Mon Feb 10 17:20:11 2014 +0100 @@ -10,7 +10,7 @@ begin typedecl nat -arities nat :: "term" +instance nat :: "term" .. axiomatization Zero :: nat ("0") and