src/Pure/Isar/isar_syn.ML
changeset 24219 e558fe311376
parent 24174 59a5ffec7078
child 24314 665b3ab2dabe
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Aug 10 17:04:24 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Aug 10 17:04:34 2007 +0200
     1.3 @@ -89,7 +89,7 @@
     1.4      (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
     1.5          P.!!! (P.list1 P.xname)) []
     1.6          -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
     1.7 -      >> (fn (x, y) => Toplevel.theory (snd o ClassPackage.axclass_cmd x y)));
     1.8 +      >> (fn (x, y) => Toplevel.theory (snd o Class.axclass_cmd x y)));
     1.9  
    1.10  
    1.11  (* types *)
    1.12 @@ -422,16 +422,16 @@
    1.13      -- P.opt_begin
    1.14      >> (fn (((bname, add_consts), (supclasses, elems)), begin) =>
    1.15          Toplevel.begin_local_theory begin
    1.16 -          (ClassPackage.class_cmd bname supclasses elems add_consts #-> TheoryTarget.begin)));
    1.17 +          (Class.class_cmd bname supclasses elems add_consts #-> TheoryTarget.begin)));
    1.18  
    1.19  val instanceP =
    1.20    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((
    1.21        P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    1.22 -           >> ClassPackage.instance_class_cmd
    1.23 +           >> Class.instance_class_cmd
    1.24        || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    1.25 -           >> ClassPackage.instance_sort_cmd
    1.26 +           >> Class.instance_sort_cmd
    1.27        || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    1.28 -           >> (fn (arities, defs) => ClassPackage.instance_arity_cmd arities defs)
    1.29 +           >> (fn (arities, defs) => Class.instance_arity_cmd arities defs)
    1.30      ) >> (Toplevel.print oo Toplevel.theory_to_proof));
    1.31  
    1.32  end;
    1.33 @@ -441,7 +441,7 @@
    1.34  
    1.35  val code_datatypeP =
    1.36    OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
    1.37 -    (Scan.repeat1 P.term >> (Toplevel.theory o CodegenData.add_datatype_consts_cmd));
    1.38 +    (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_consts_cmd));
    1.39  
    1.40  
    1.41  
    1.42 @@ -763,7 +763,7 @@
    1.43  val print_classesP =
    1.44    OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag
    1.45      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
    1.46 -      o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of)));
    1.47 +      o Toplevel.keep (Class.print_classes o Toplevel.theory_of)));
    1.48  
    1.49  val print_localeP =
    1.50    OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag
    1.51 @@ -884,7 +884,7 @@
    1.52    OuterSyntax.improper_command "print_codesetup" "print code generator setup of this theory" K.diag
    1.53      (Scan.succeed
    1.54        (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
    1.55 -        (CodegenData.print_codesetup o Toplevel.theory_of)));
    1.56 +        (Code.print_codesetup o Toplevel.theory_of)));
    1.57  
    1.58  
    1.59  (** system commands (for interactive mode only) **)