src/Pure/Isar/isar_syn.ML
changeset 38379 67d71449e85b
parent 38350 480b2de9927c
child 38708 8915e3ce8655
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Aug 11 15:45:15 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 11 16:02:03 2010 +0200
     1.3 @@ -462,11 +462,11 @@
     1.4     (Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin
     1.5      >> (fn ((name, (supclasses, elems)), begin) =>
     1.6          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
     1.7 -          (Class.class_cmd name supclasses elems #> snd)));
     1.8 +          (Class_Declaration.class_cmd name supclasses elems #> snd)));
     1.9  
    1.10  val _ =
    1.11    Outer_Syntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal
    1.12 -    (Parse.xname >> Class.subclass_cmd);
    1.13 +    (Parse.xname >> Class_Declaration.subclass_cmd);
    1.14  
    1.15  val _ =
    1.16    Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl