src/HOL/UNITY/Extend.thy

--- a/src/HOL/UNITY/Extend.thy	Mon Oct 11 10:52:51 1999 +0200
+++ b/src/HOL/UNITY/Extend.thy	Mon Oct 11 10:53:39 1999 +0200
@@ -23,7 +23,7 @@
     "project_set h C == {x. EX y. h(x,y) : C}"
 
   extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
-    "extend_act h act == UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
+    "extend_act h == %act. UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
 
   (*Argument C allows weak safety laws to be projected*)
   project_act :: "['c set, 'a*'b => 'c, ('c*'c) set] => ('a*'a) set"