# HG changeset patch
# User wenzelm
# Date 1144922472 -7200
# Node ID 87cbbe045ea5e067d9de22e1b7638d6c8a969900
# Parent  c7a2b7a8c4cbdf9454705f2861c968a45801ef46
add_axclass(_i): canonical specification format;

diff -r c7a2b7a8c4cb -r 87cbbe045ea5 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Thu Apr 13 12:01:11 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Thu Apr 13 12:01:12 2006 +0200
@@ -328,10 +328,8 @@
 
 fun add_axclass_i (name, supsort) axs thy =
   let
-    fun rearrange_axioms ((name, atts), ts) =
-      map (rpair atts o pair "") ts;
     val (c, thy') = thy
-      |> AxClass.add_axclass_i (name, supsort) [] ((Library.flat o map rearrange_axioms) axs);
+      |> AxClass.add_axclass_i (name, supsort) [] axs;
     val {intro, axioms, ...} = AxClass.get_info thy' c;
   in ((c, (intro, axioms)), thy') end;
 
@@ -423,7 +421,7 @@
     #-> (fn mapp_this =>
           `(fn thy => extract_assumes thy name_locale (mapp_sup @ mapp_this))
     #-> (fn loc_axioms =>
-          add_axclass_i (bname, supsort) loc_axioms
+          add_axclass_i (bname, supsort) (map (apfst (apfst (K ""))) loc_axioms)
     #-> (fn (name_axclass, (_, ax_axioms)) =>
           fold (add_global_constraint v name_axclass) mapp_this
     #> add_class_data (name_locale, (supclasses, name_locale, name_axclass, intro, v, mapp_this))