sect: exlude ":" from parser;
authorwenzelm
Wed Mar 08 23:46:59 2000 +0100 (2000-03-08)
changeset 83814fc7e63781f6
parent 8380 c96953faf0a4
child 8382 52d5fae273dd
sect: exlude ":" from parser;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Wed Mar 08 23:45:37 2000 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Wed Mar 08 23:46:59 2000 +0100
     1.3 @@ -458,7 +458,7 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun sect ss = Scan.first (map (fn s => Scan.lift (s --| Args.$$$ ":")) ss);
     1.8 +fun sect ss = Scan.first (map Scan.lift ss);
     1.9  fun thms ss = Scan.unless (sect ss) Attrib.local_thms;
    1.10  fun thmss ss = Scan.repeat (thms ss) >> flat;
    1.11