removed obsolete Locale.smart_theorem;

--- a/src/Pure/Isar/isar_syn.ML	Tue Nov 07 19:39:46 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Nov 07 19:39:48 2006 +0100
@@ -389,8 +389,7 @@
       P.general_statement >> (fn ((loc, a), (elems, concl)) =>
       (Toplevel.print o
        Toplevel.local_theory_to_proof loc
-         (Specification.theorem kind NONE (K I) a elems concl) o
-       Toplevel.theory_to_proof (Locale.smart_theorem kind loc a elems concl))));
+         (Specification.theorem kind NONE (K I) a elems concl))));
 
 val theoremP = gen_theorem PureThy.theoremK;
 val lemmaP = gen_theorem PureThy.lemmaK;