--- a/src/HOL/UNITY/Extend.thy Mon Oct 18 15:20:21 1999 +0200
+++ b/src/HOL/UNITY/Extend.thy Mon Oct 18 16:16:03 1999 +0200
@@ -33,8 +33,8 @@
extend_act h `` Acts F)"
(*Argument C allows weak safety laws to be projected*)
- project :: "['c set, 'a*'b => 'c, 'c program] => 'a program"
- "project C h F == mk_program (project_set h (Init F),
+ project :: "['a*'b => 'c, 'c set, 'c program] => 'a program"
+ "project h C F == mk_program (project_set h (Init F),
project_act h `` Restrict C `` Acts F)"
locale Extend =