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