--- a/Matcher.thy	Tue Apr 19 02:19:56 2011 +0000
+++ b/Matcher.thy	Tue Apr 19 02:25:21 2011 +0000
@@ -2,15 +2,6 @@
   imports "Main" 
 begin
 
-term "TYPE (nat * int)"
-term "TYPE ('a)"
-
-definition
-  P:: "'a itself \<Rightarrow> bool"
-where
-  "P (TYPE ('a)) \<equiv> ((\<lambda>x. (x::'a)) = (\<lambda>x. x))"
-
-
 section {* Sequential Composition of Sets *}
 
 definition