--- a/ex/PL0.thy	Wed Jun 29 12:04:04 1994 +0200
+++ b/ex/PL0.thy	Fri Jul 08 12:01:55 1994 +0200
@@ -7,12 +7,6 @@
 *)
 
 PL0 = HOL +
-types 'a pl
-arities pl :: (term)term
-consts
-    false	:: "'a pl"
-    "->"	:: "['a pl,'a pl] => 'a pl"	(infixr 90)
-    var		:: "'a => 'a pl"		("#_")
 datatype
-    'a pl = false | var('a) | "op->" ('a pl,'a pl)
+    'a pl = false | var ('a) ("#_") | "->" ('a pl,'a pl) (infixr 90)
 end