diff -r 69d815b0e1eb -r 21291189b51e ex/PL.thy
--- a/ex/PL.thy	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/PL.thy	Wed Mar 02 12:26:55 1994 +0100
@@ -46,7 +46,7 @@
 eval_def "tt[p] == pl_rec(p, %v.v:tt, False, op -->)"
 
 hyps_def
- "hyps(p,tt) == pl_rec(p, %a. {if(a:tt, #a, #a->false)}, {}, op Un)"
+ "hyps(p,tt) == pl_rec(p, %a. {if(a:tt, #a, (#a)->false)}, {}, op Un)"
 
 var_inject "(#v = #w) ==> v = w"
 imp_inject "[| (p -> q) = (p' -> q'); [| p = p'; q = q' |] ==> R |] ==> R"