# HG changeset patch
# User haftmann
# Date 1205182306 -3600
# Node ID f2cd4bf1e40429e15646c81e16f805c91d18f8d5
# Parent  b6608fbeaae1f1b0bb7a4c184de0b5d33502a364
dropped "include" feature of classes

diff -r b6608fbeaae1 -r f2cd4bf1e404 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Mar 10 21:51:45 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Mar 10 21:51:46 2008 +0100
@@ -427,8 +427,8 @@
 
 val class_val =
   SpecParse.class_expr --
-    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.locale_element)) [] ||
-  Scan.repeat1 SpecParse.locale_element >> pair [];
+    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
+  Scan.repeat1 SpecParse.context_element >> pair [];
 
 val _ =
   OuterSyntax.command "class" "define type class" K.thy_decl