# HG changeset patch
# User wenzelm
# Date 1160861151 -7200
# Node ID 82f44ceb4fa3e2c64c60908e63d273ebbe5f5234
# Parent  a4b85340d6bdf7019a48b9c83ccfce79c8c2c527
theorem: added local_theory version;

diff -r a4b85340d6bd -r 82f44ceb4fa3 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Oct 14 23:25:51 2006 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Oct 14 23:25:51 2006 +0200
@@ -386,8 +386,11 @@
   OuterSyntax.command kind ("state " ^ kind) K.thy_goal
     (P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --|
       Scan.ahead (P.locale_keyword || P.statement_keyword)) ("", []) --
-      P.general_statement >> (fn ((x, y), (z, w)) =>
-      (Toplevel.print o Toplevel.theory_to_proof (Locale.smart_theorem kind x y z w))));
+      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))));
 
 val theoremP = gen_theorem PureThy.theoremK;
 val lemmaP = gen_theorem PureThy.lemmaK;