changeset 5596 | b29d18d8c4d2 |
parent 5584 | aad639e56d4e |
child 6012 | 1894bfc4aee9 |
--- a/src/HOL/UNITY/NSP_Bad.thy Thu Oct 01 18:27:55 1998 +0200 +++ b/src/HOL/UNITY/NSP_Bad.thy Thu Oct 01 18:28:18 1998 +0200 @@ -54,7 +54,6 @@ constdefs Nprg :: state program (*Initial trace is empty*) - "Nprg == (|Init = {[]}, - Acts0 = {Fake, NS1, NS2, NS3}|)" + "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3})" end