# HG changeset patch
# User haftmann
# Date 1232577623 -3600
# Node ID 83d282f12352733d7da8876427237acb911fad96
# Parent  a010aab5bed03d5925052a27e214ea677b0f7f3a
allow empty class specs

diff -r a010aab5bed0 -r 83d282f12352 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Wed Jan 21 23:40:23 2009 +0100
@@ -55,8 +55,6 @@
     -> (Attrib.binding * string list) list
     -> theory -> class * theory
   val classrel_cmd: xstring * xstring -> theory -> Proof.state
-
-  (*old instance layer*)
   val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state
   val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state
 end;
@@ -275,7 +273,7 @@
     val intros = (snd o rules thy) sup :: map_filter I
       [Option.map (Drule.standard' o Element.conclude_witness) some_wit,
         (fst o rules thy) sub];
-    val tac = ALLGOALS (EVERY' (map Tactic.rtac intros));
+    val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
     val classrel = Goal.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
       (K tac);
     val diff_sort = Sign.complete_sort thy [sup]
@@ -285,9 +283,9 @@
     |> AxClass.add_classrel classrel
     |> ClassData.map (Graph.add_edge (sub, sup))
     |> activate_defs sub (these_defs thy diff_sort)
-    |> fold2 (fn dep_morph => fn wit => Locale.add_dependency sub (sup,
-        dep_morph $> Element.satisfy_morphism [wit] $> export))
-          (the_list some_dep_morph) (the_list some_wit)
+    |> fold (fn dep_morph => Locale.add_dependency sub (sup,
+        dep_morph $> Element.satisfy_morphism (the_list some_wit) $> export))
+          (the_list some_dep_morph)
     |> (fn thy => fold_rev Locale.activate_global_facts
       (Locale.get_registrations thy) thy)
   end;
diff -r a010aab5bed0 -r 83d282f12352 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Jan 21 23:40:23 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jan 21 23:40:23 2009 +0100
@@ -428,7 +428,7 @@
 
 val _ =
   OuterSyntax.command "class" "define type class" K.thy_decl
-   (P.name -- (P.$$$ "=" |-- class_val) -- P.opt_begin
+   (P.name -- Scan.optional (P.$$$ "=" |-- class_val) ([], []) -- P.opt_begin
     >> (fn ((name, (supclasses, elems)), begin) =>
         (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
           (Class.class_cmd name supclasses elems #> snd)));