# HG changeset patch
# User wenzelm
# Date 1160353201 -7200
# Node ID 9673c67dde9ba8402be5543882f3ea36ff05a67a
# Parent  63150f3a103da81ff2290588e74e4bcc0a022469
lemmas/theorems/declare: Specification.theorems;

diff -r 63150f3a103d -r 9673c67dde9b src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Oct 09 02:19:58 2006 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Oct 09 02:20:01 2006 +0200
@@ -241,7 +241,7 @@
 (* theorems *)
 
 fun theorems kind = P.opt_locale_target -- P.name_facts
-  >> (Toplevel.theory_context o uncurry (IsarThy.smart_theorems kind));
+  >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems kind args));
 
 val theoremsP =
   OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems PureThy.theoremK);
@@ -252,7 +252,8 @@
 val declareP =
   OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
     (P.opt_locale_target -- (P.and_list1 P.xthms1 >> flat)
-      >> (Toplevel.theory_context o uncurry IsarThy.declare_theorems));
+      >> (fn (loc, args) => Toplevel.local_theory loc
+          (#2 o Specification.theorems "" [(("", []), args)])));
 
 
 (* name space entry path *)