added Id_apply

--- a/src/HOL/Fun.ML	Wed Sep 09 16:42:45 1998 +0200
+++ b/src/HOL/Fun.ML	Wed Sep 09 16:43:14 1998 +0200
@@ -31,6 +31,12 @@
 qed "bchoice";
 
 
+section "Id";
+
+qed_goalw "Id_apply" thy [Id_def] "Id x = x" (K [rtac refl 1]);
+Addsimps [Id_apply];
+
+
 section "o";
 
 qed_goalw "o_apply" thy [o_def] "(f o g) x = f (g x)"