# HG changeset patch
# User wenzelm
# Date 1185566120 -7200
# Node ID 2ef318813e1a89b3c702acb3fddddbe39332b5c7
# Parent  85bb54571031b2b14c65a3bed503c8aba99864a5
method section scanners: added [[declaration]] syntax, ignore sid-effects of thms;

diff -r 85bb54571031 -r 2ef318813e1a src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Jul 27 21:55:19 2007 +0200
+++ b/src/Pure/Isar/method.ML	Fri Jul 27 21:55:20 2007 +0200
@@ -465,13 +465,11 @@
 
 local
 
-fun sect ss = Scan.first (map Scan.lift ss);
-fun thms ss = Scan.repeat (Scan.unless (sect ss) Attrib.multi_thm) >> flat;
-
+fun thms ss = Scan.repeat (Scan.unless (Scan.lift (Scan.first ss)) Attrib.multi_thm) >> flat;
 fun app (f, att) (context, ths) = foldl_map att (Context.map_proof f context, ths);
 
-fun section ss = (sect ss -- thms ss) :-- (fn (m, ths) => Scan.depend (fn context =>
-  Scan.succeed (app m (context, ths)))) >> #2;
+fun section ss = Scan.depend (fn context => (Scan.first ss -- Scan.pass context (thms ss)) :--
+  (fn (m, ths) => Scan.succeed (app m (context, ths))) >> #2);
 
 fun sectioned args ss = args -- Scan.repeat (section ss);