dropped "include" feature of classes
authorhaftmann
Mon Mar 10 21:51:46 2008 +0100 (2008-03-10 ago)
changeset 26248f2cd4bf1e404
parent 26247 b6608fbeaae1
child 26249 59ecf1ce8222
dropped "include" feature of classes
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Mar 10 21:51:45 2008 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Mar 10 21:51:46 2008 +0100
     1.3 @@ -427,8 +427,8 @@
     1.4  
     1.5  val class_val =
     1.6    SpecParse.class_expr --
     1.7 -    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.locale_element)) [] ||
     1.8 -  Scan.repeat1 SpecParse.locale_element >> pair [];
     1.9 +    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
    1.10 +  Scan.repeat1 SpecParse.context_element >> pair [];
    1.11  
    1.12  val _ =
    1.13    OuterSyntax.command "class" "define type class" K.thy_decl