src/Pure/Isar/isar_syn.ML
changeset 22321 e5cddafe2629
parent 22299 a1293efe7ea5
child 22331 7df6bc8cf0b0
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Feb 14 10:06:16 2007 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Feb 14 10:06:17 2007 +0100
     1.3 @@ -427,14 +427,16 @@
     1.4      -- P.opt_begin
     1.5      >> (fn ((bname, (supclasses, elems)), begin) =>
     1.6          Toplevel.begin_local_theory begin
     1.7 -          (ClassPackage.class_e bname supclasses elems #-> TheoryTarget.begin true)));
     1.8 +          (ClassPackage.class_cmd bname supclasses elems #-> TheoryTarget.begin true)));
     1.9  
    1.10  val instanceP =
    1.11    OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
    1.12        P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    1.13 -           >> ClassPackage.instance_sort_e
    1.14 +           >> ClassPackage.instance_class_cmd
    1.15 +      || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    1.16 +           >> ClassPackage.instance_sort_cmd (*experimental: by interpretation of locales*)
    1.17        || P.and_list1 parse_arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    1.18 -           >> (fn (arities, defs) => ClassPackage.instance_arity_e arities defs)
    1.19 +           >> (fn (arities, defs) => ClassPackage.instance_arity_cmd arities defs)
    1.20      ) >> (Toplevel.print oo Toplevel.theory_to_proof));
    1.21  
    1.22  val print_classesP =