# HG changeset patch
# User wenzelm
# Date 1144622034 -7200
# Node ID edf92521e8d39961389122f3a7196986b33ec325
# Parent  9f69613362c193145e65a9fa2f4bcbe1ce3e31d9
simplified AxClass.add_axclass interface;

diff -r 9f69613362c1 -r edf92521e8d3 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Mon Apr 10 00:33:53 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Mon Apr 10 00:33:54 2006 +0200
@@ -330,14 +330,11 @@
 fun add_axclass_i (name, supsort) axs thy =
   let
     fun rearrange_axioms ((name, atts), ts) =
-      map (rpair atts o pair "") ts
-  in
-    thy
-    |> AxClass.add_axclass_i (name, supsort)
-          ((Library.flat o map rearrange_axioms) axs)
-    |-> (fn { intro, axioms } =>
-              pair (Sign.full_name thy name, (intro, axioms)))
-  end;
+      map (rpair atts o pair "") ts;
+    val (c, thy') = thy
+      |> AxClass.add_axclass_i (name, supsort) ((Library.flat o map rearrange_axioms) axs);
+    val {intro, axioms, ...} = AxClass.get_info thy' c;
+  in ((c, (intro, axioms)), thy') end;
 
 fun prove_interpretation_i (prfx, atts) expr insts tac thy =
   let