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.
'declare': and_list1;
authorwenzelm
Wed, 27 Feb 2002 21:52:41 +0100
changeset 12968 e4002554cbfb
parent 12967 c61def7021e8
child 12969 d860fa102386
'declare': and_list1; 'obtain': updated;
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_syn.ML	Wed Feb 27 19:44:22 2002 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Feb 27 21:52:41 2002 +0100
@@ -196,7 +196,8 @@
 
 val declareP =
   OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
-    (P.locale_target -- P.xthms1 >> (Toplevel.theory o uncurry IsarThy.declare_theorems));
+    (P.locale_target -- (P.and_list1 P.xthms1 >> flat)
+      >> (Toplevel.theory o uncurry IsarThy.declare_theorems));
 
 
 (* name space entry path *)
@@ -376,8 +377,7 @@
     K.prf_asm_goal
     (Scan.optional
       (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ))
-        --| P.$$$ "where") [] -- statement
-    >> (Toplevel.print oo (Toplevel.proof o IsarThy.obtain)));
+        --| P.$$$ "where") [] -- statement >> (Toplevel.print oo IsarThy.obtain));
 
 val letP =
   OuterSyntax.command "let" "bind text variables" K.prf_decl
isabelle