src/Pure/Isar/isar_syn.ML
changeset 35315 fbdc860d87a3
parent 35223 9f35be9c2960
child 35351 7425aece4ee3
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Feb 22 17:02:39 2010 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Feb 23 10:11:12 2010 +0100
     1.3 @@ -99,13 +99,6 @@
     1.4    OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
     1.5      (P.sort >> (Toplevel.theory o Sign.add_defsort));
     1.6  
     1.7 -val _ =
     1.8 -  OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
     1.9 -    (P.binding -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
    1.10 -        P.!!! (P.list1 P.xname)) []
    1.11 -        -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
    1.12 -      >> (fn (x, y) => Toplevel.theory (snd o Class.axclass_cmd x y)));
    1.13 -
    1.14  
    1.15  (* types *)
    1.16