Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
lemmas/theorems/declare: Specification.theorems;
authorwenzelm
Mon, 09 Oct 2006 02:20:01 +0200
changeset 20907 9673c67dde9b
parent 20906 63150f3a103d
child 20908 5f7458cc4f67
lemmas/theorems/declare: Specification.theorems;
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle