src/Pure/Isar/isar_syn.ML
changeset 51685 385ef6706252
parent 51658 21c10672633b
child 51717 9e7d1c139569
--- a/src/Pure/Isar/isar_syn.ML	Wed Apr 10 13:10:38 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 10 15:30:19 2013 +0200
@@ -79,13 +79,13 @@
   Outer_Syntax.command @{command_spec "classes"} "declare type classes"
     (Scan.repeat1 (Parse.binding -- Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<"}) |--
         Parse.!!! (Parse.list1 Parse.class)) [])
-      >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
+      >> (Toplevel.theory o fold Axclass.axiomatize_class_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "classrel"} "state inclusion of type classes (axiomatic!)"
     (Parse.and_list1 (Parse.class -- ((@{keyword "\<subseteq>"} || @{keyword "<"})
         |-- Parse.!!! Parse.class))
-    >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
+    >> (Toplevel.theory o Axclass.axiomatize_classrel_cmd));
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "default_sort"}
@@ -113,7 +113,7 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "arities"} "state type arities (axiomatic!)"
-    (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));
+    (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold Axclass.axiomatize_arity_cmd));
 
 
 (* consts and syntax *)