dropped "include" feature of classes
authorhaftmann
Mon, 10 Mar 2008 21:51:46 +0100
changeset 26248 f2cd4bf1e404
parent 26247 b6608fbeaae1
child 26249 59ecf1ce8222
dropped "include" feature of classes
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