diff -r e4fbf438376d -r edc90be09ac1 src/HOL/UNITY/Project.thy
--- a/src/HOL/UNITY/Project.thy	Fri Aug 03 16:28:25 2007 +0200
+++ b/src/HOL/UNITY/Project.thy	Fri Aug 03 20:19:41 2007 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/Project.ML
+(*  Title:      HOL/UNITY/Project.thy
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1999  University of Cambridge
@@ -673,21 +673,4 @@
 apply (blast intro: project_LeadsTo_D)
 done
 
-ML
-{*
-val projecting_Int = thm "projecting_Int";
-val projecting_Un = thm "projecting_Un";
-val projecting_INT = thm "projecting_INT";
-val projecting_UN = thm "projecting_UN";
-val projecting_weaken = thm "projecting_weaken";
-val projecting_weaken_L = thm "projecting_weaken_L";
-val extending_Int = thm "extending_Int";
-val extending_Un = thm "extending_Un";
-val extending_INT = thm "extending_INT";
-val extending_UN = thm "extending_UN";
-val extending_weaken = thm "extending_weaken";
-val extending_weaken_L = thm "extending_weaken_L";
-val projecting_UNIV = thm "projecting_UNIV";
-*}
-
 end