# HG changeset patch
# User nipkow
# Date 783189700 -3600
# Node ID 368aa02631d86918b87ace9787c7963d27914e3d
# Parent  2b16819fbd7188a27804c6f19b43e82420fc68b6
removed superfluous type_intrs in datatype com.

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.*)