src/Pure/Isar/isar_syn.ML

 val axclassP =
   OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
     (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
         P.!!! (P.list1 P.xname)) []
         -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
-      >> (fn (x, y) => Toplevel.theory (snd o AxClass.define_class x [] y)));
+      >> (fn (x, y) => Toplevel.theory (snd o ClassPackage.axclass_cmd x y)));
 
 
 (* types *)
 
 val typedeclP =

            >> ClassPackage.instance_sort_cmd (*experimental: by interpretation of locales*)
       || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
            >> (fn (arities, defs) => ClassPackage.instance_arity_cmd arities defs)
     ) >> (Toplevel.print oo Toplevel.theory_to_proof));
 
-val print_classesP =
-  OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
-      o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of)));
-
 end;
 
 
 
 (** proof commands **)

   OuterSyntax.improper_command "kill" "kill current history node" K.control
     (Scan.succeed ((Toplevel.no_timing o Toplevel.print) o IsarCmd.kill));
 
 
 
+(** code generation **)
+
+val code_datatypeP =
+  OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl (
+    Scan.repeat1 P.term
+    >> (Toplevel.theory o CodegenData.add_datatype_consts_cmd)
+  );
+
+
+
 (** diagnostic commands (for interactive mode only) **)
 
 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
 val opt_bang = Scan.optional (P.$$$ "!" >> K true) false;
 

     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems));
 
 val print_localesP =
   OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
+
+val print_classesP =
+  OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
+    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
+      o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of)));
 
 val print_localeP =
   OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
     (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale));
 

 
 val print_typeP =
   OuterSyntax.improper_command "typ" "read and print type" K.diag
     (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
 
+val print_codesetupP =
+  OuterSyntax.improper_command "print_codesetup" "print code generator setup of this theory" K.diag
+    (Scan.succeed
+      (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
+        (CodegenData.print_codesetup o Toplevel.theory_of)));
 
 
 (** system commands (for interactive mode only) **)
 
 val cdP =

   qedP, terminal_proofP, default_proofP, immediate_proofP,
   done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP,
   apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
   cannot_undoP, redoP, undos_proofP, undoP, killP, interpretationP,
   interpretP,
+  (*code generation*)
+  code_datatypeP,
   (*diagnostic commands*)
   pretty_setmarginP, helpP, print_classesP, print_commandsP, print_contextP,
   print_theoryP, print_syntaxP, print_abbrevsP, print_factsP,
   print_theoremsP, print_localesP, print_localeP,
   print_registrationsP, print_attributesP, print_simpsetP,
   print_rulesP, print_induct_rulesP, print_trans_rulesP,
   print_methodsP, print_antiquotationsP, thy_depsP, class_depsP, thm_depsP,
   find_theoremsP, print_bindsP, print_casesP, print_stmtsP,
   print_thmsP, print_prfsP, print_full_prfsP, print_propP,
-  print_termP, print_typeP,
+  print_termP, print_typeP, print_codesetupP,
   (*system commands*)
   cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
   touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,
   kill_thyP, display_draftsP, print_draftsP, prP, disable_prP,
   enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];