src/HOL/UNITY/Common.ML
changeset 5608 a82a038a3e7a
parent 5584 aad639e56d4e
child 5620 3ac11c4af76a
--- a/src/HOL/UNITY/Common.ML	Fri Oct 02 10:44:20 1998 +0200
+++ b/src/HOL/UNITY/Common.ML	Fri Oct 02 14:28:39 1998 +0200
@@ -31,7 +31,7 @@
 (*** Some programs that implement the safety property above ***)
 
 (*This one is just Skip*)
-Goal "constrains {id} {m} (maxfg m)";
+Goal "constrains {Id} {m} (maxfg m)";
 by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
 				  fasc, gasc]) 1);
 result();