avoid referencing thy value;
rename_numerals: use implicit theory context;
eliminated some simpset_of Int.thy (why needed anyway?);
(*<*)
theory fakenat = Main:;
(*>*)
text{*\noindent
The type \isaindexbold{nat} of natural numbers is predefined and
behaves like
*}
datatype nat = "0" | Suc nat
(*<*)
end
(*>*)