diff -r 2b16819fbd71 -r 368aa02631d8 src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Wed Oct 26 15:20:55 1994 +0100
+++ b/src/ZF/IMP/Com.thy	Wed Oct 26 17:41:40 1994 +0100
@@ -84,7 +84,6 @@
         | semic ("c0:com", "c1:com")		("_; _"  [60, 60] 10)
 	| while ("b:bexp", "c:com")		("while _ do _"  60)
 	| ifc   ("b:bexp", "c0:com", "c1:com")	("ifc _ then _ else _"  60)
-  type_intrs "aexp.intrs"
 
 (*Constructor ";" has low precedence to avoid syntactic ambiguities
   with [| m: nat; x: loc; ... |] ==> ...  It usually will need parentheses.*)