# 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