src/Pure/Isar/method.ML
changeset 8381 4fc7e63781f6
parent 8372 7b2cec1e789c
child 8519 981f52707e5d
     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