# HG changeset patch
# User wenzelm
# Date 1014843161 -3600
# Node ID e4002554cbfbd7dd5aaa4c4d5f4043cbd4b0ff56
# Parent  c61def7021e8ac381d8e3cd0433a407fdbfcb97b
'declare': and_list1;
'obtain': updated;

diff -r c61def7021e8 -r e4002554cbfb src/Pure/Isar/isar_syn.ML
--- 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