diff -r bcd0ee8d71aa -r 8c9be2e9236d ex/PL.thy
--- a/ex/PL.thy	Fri Jul 08 17:22:58 1994 +0200
+++ b/ex/PL.thy	Fri Jul 08 17:39:02 1994 +0200
@@ -6,7 +6,9 @@
 Inductive definition of propositional logic.
 *)
 
-PL = Finite + PL0 +
+PL = Finite +
+datatype
+    'a pl = false | var ('a) ("#_" [1000]) | "->" ('a pl,'a pl) (infixr 90)
 consts
     axK,axS,axDN:: "'a pl set"
     ruleMP,thms :: "'a pl set => 'a pl set"
@@ -40,6 +42,6 @@
     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)"
 
 end