# HG changeset patch
# User wenzelm
# Date 773491796 -7200
# Node ID 75ac32497f09b5f5a90940f7edc4aff5ca6807c7
# Parent  d7ff85d292c7ef19698b2d2c5b49e1cf03de4899
various minor changes (names and comments);

diff -r d7ff85d292c7 -r 75ac32497f09 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Jul 06 11:53:30 1994 +0200
+++ b/src/Pure/axclass.ML	Wed Jul 06 12:49:56 1994 +0200
@@ -3,6 +3,10 @@
     Author:     Markus Wenzel, TU Muenchen
 
 Higher level user interfaces for axiomatic type classes.
+
+TODO:
+  remove add_sigclass (?)
+  remove goal_... (?)
 *)
 
 signature AX_CLASS =
@@ -25,9 +29,9 @@
       -> tactic option -> thm
     val prove_arity: theory -> string * sort list * class -> thm list
       -> tactic option -> thm
-    val add_subclass: class * class -> string list -> thm list
+    val add_inst_subclass: class * class -> string list -> thm list
       -> tactic option -> theory -> theory
-    val add_instance: string * sort list * class list -> string list
+    val add_inst_arity: string * sort list * class list -> string list
       -> thm list -> tactic option -> theory -> theory
   end
 end;
@@ -102,7 +106,7 @@
 
 fun mk_arity (t, ss, c) =
   let
-    val names = variantlist (replicate (length ss) "'a", []);
+    val names = tl (variantlist (replicate (length ss + 1) "'", []));
     val tfrees = map TFree (names ~~ ss);
   in
     mk_inclass (Type (t, tfrees), c)
@@ -310,13 +314,13 @@
 
 
 
-(** add proved class relations and instances **)
+(** add proved subclass relations and arities **)
 
-fun add_subclass (c1, c2) axms thms usr_tac thy =
+fun add_inst_subclass (c1, c2) axms thms usr_tac thy =
   add_classrel_thms
   [prove_classrel thy (c1, c2) (get_axioms thy axms @ thms) usr_tac] thy;
 
-fun add_instance (t, ss, cs) axms thms usr_tac thy =
+fun add_inst_arity (t, ss, cs) axms thms usr_tac thy =
   let
     val usr_thms = get_axioms thy axms @ thms;
     fun prove c =