# HG changeset patch
# User haftmann
# Date 1192192951 -7200
# Node ID 0b067b2d1b8834840d979fe46ff917784d71f458
# Parent  c3d9cb3904715d05bb37c28204d59fa3a9394407
dropped local_syntax

diff -r c3d9cb390471 -r 0b067b2d1b88 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Oct 12 14:42:30 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Oct 12 14:42:31 2007 +0200
@@ -23,7 +23,7 @@
   "advanced", "and", "assumes", "attach", "begin", "binder", "concl",
   "constrains", "defines", "fixes", "for", "identifier", "if",
   "imports", "in", "includes", "infix", "infixl", "infixr", "is",
-  "local_syntax", "notes", "obtains", "open", "output", "overloaded", "shows",
+  "notes", "obtains", "open", "output", "overloaded", "shows",
   "structure", "unchecked", "uses", "where", "|"];
 
 
@@ -434,11 +434,10 @@
   OuterSyntax.command "class" "define type class" K.thy_decl
    (P.name --
      Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") [] --  (* FIXME ?? *)
-     Scan.optional (P.$$$ "(" |-- (P.$$$ "local_syntax" >> K true) --| P.$$$ ")") false --  (* FIXME ?? *)
      (P.$$$ "=" |-- class_val) -- P.opt_begin
-    >> (fn ((((name, add_consts), local_syntax), (supclasses, elems)), begin) =>
+    >> (fn (((name, add_consts), (supclasses, elems)), begin) =>
         (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
-          (Class.class_cmd false name supclasses elems add_consts #-> TheoryTarget.begin)));
+          (Class.class_cmd name supclasses elems add_consts #-> TheoryTarget.begin)));
 
 val _ =
   OuterSyntax.command "subclass" "prove a subclass relation" K.thy_goal