Specification.theorem now also takes "interactive" flag as argument.

--- a/src/Pure/Isar/isar_syn.ML	Tue Aug 28 16:33:52 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Aug 28 18:01:37 2007 +0200
@@ -455,7 +455,7 @@
       Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) ("", []) --
       SpecParse.general_statement >> (fn ((loc, a), (elems, concl)) =>
       (Toplevel.print o
-       Toplevel.local_theory_to_proof loc
+       Toplevel.local_theory_to_proof' loc
          (Specification.theorem kind NONE (K I) a elems concl))));
 
 val theoremP = gen_theorem Thm.theoremK;