# HG changeset patch
# User wenzelm
# Date 1003431746 -7200
# Node ID ef3e51b1b4ec28572b5530a84c23040c72f72092
# Parent  16ef206e6648a277892518ea4b2f5e895717ec33
sane internal interfaces for instance;

diff -r 16ef206e6648 -r ef3e51b1b4ec src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Thu Oct 18 21:01:59 2001 +0200
+++ b/src/Pure/axclass.ML	Thu Oct 18 21:02:26 2001 +0200
@@ -16,14 +16,14 @@
     -> theory -> theory * {intro: thm, axioms: thm list}
   val add_axclass_i: bclass * class list -> ((bstring * term) * theory attribute list) list
     -> theory -> theory * {intro: thm, axioms: thm list}
-  val add_inst_subclass: xclass * xclass -> string list -> thm list
-    -> tactic option -> theory -> theory
-  val add_inst_subclass_i: class * class -> string list -> thm list
+  val add_inst_subclass_x: xclass * xclass -> string list -> thm list
     -> tactic option -> theory -> theory
-  val add_inst_arity: xstring * string list * string -> string list
+  val add_inst_subclass: xclass * xclass -> tactic -> theory -> theory
+  val add_inst_subclass_i: class * class -> tactic -> theory -> theory
+  val add_inst_arity_x: xstring * string list * string -> string list
     -> thm list -> tactic option -> theory -> theory
-  val add_inst_arity_i: string * sort list * sort -> string list
-    -> thm list -> tactic option -> theory -> theory
+  val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory
+  val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
   val default_intro_classes_tac: thm list -> int -> tactic
   val axclass_tac: thm list -> tactic
   val prove_subclass: theory -> class * class -> thm list
@@ -417,11 +417,15 @@
         prove_arity thy (t, Ss, c) wthms usr_tac);
   in add_arity_thms (map prove cs) thy end;
 
+fun sane_inst_subclass prep sub tac = ext_inst_subclass prep sub [] [] (Some tac);
+fun sane_inst_arity prep arity tac = ext_inst_arity prep arity [] [] (Some tac);
 
-val add_inst_subclass = ext_inst_subclass read_classrel;
-val add_inst_subclass_i = ext_inst_subclass cert_classrel;
-val add_inst_arity = ext_inst_arity read_arity;
-val add_inst_arity_i = ext_inst_arity cert_arity;
+val add_inst_subclass_x = ext_inst_subclass read_classrel;
+val add_inst_subclass = sane_inst_subclass read_classrel;
+val add_inst_subclass_i = sane_inst_subclass cert_classrel;
+val add_inst_arity_x = ext_inst_arity read_arity;
+val add_inst_arity = sane_inst_arity read_arity;
+val add_inst_arity_i = sane_inst_arity cert_arity;
 
 
 (* make old-style interactive goals *)