It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...
(* Title: HOL/Hoare/ROOT.ML
ID: $Id$
Author: Tobias Nipkow
Copyright 1998-2003 TUM
*)
use_thys ["Examples", "ExamplesAbort", "Pointers0", "Pointer_Examples",
"Pointer_ExamplesAbort", "SchorrWaite", "Separation"];