# HG changeset patch
# User wenzelm
# Date 952555619 -3600
# Node ID 4fc7e63781f6d10eeaaa72939f561102f3ac03ff
# Parent  c96953faf0a4ba3ffab789e31c7d9ea52bb3ce8d
sect: exlude ":" from parser;

diff -r c96953faf0a4 -r 4fc7e63781f6 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Mar 08 23:45:37 2000 +0100
+++ b/src/Pure/Isar/method.ML	Wed Mar 08 23:46:59 2000 +0100
@@ -458,7 +458,7 @@
 
 local
 
-fun sect ss = Scan.first (map (fn s => Scan.lift (s --| Args.$$$ ":")) ss);
+fun sect ss = Scan.first (map Scan.lift ss);
 fun thms ss = Scan.unless (sect ss) Attrib.local_thms;
 fun thmss ss = Scan.repeat (thms ss) >> flat;