# HG changeset patch
# User berghofe
# Date 1188316897 -7200
# Node ID 7c205d006719119701f1ed9acd3cfbbe1452c9ec
# Parent  70fd99d4ef825f0b1713aee8599373b86c496004
Specification.theorem now also takes "interactive" flag as argument.

diff -r 70fd99d4ef82 -r 7c205d006719 src/Pure/Isar/isar_syn.ML
--- 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;