# HG changeset patch
# User wenzelm
# Date 1272290884 -7200
# Node ID 7b92238454d695345b63ee24b9cfe81ee1f0e464
# Parent  f71978e47cd50814c079d0bc381ff0a9180aff97# Parent  5518de23101d302ba17ae34a14dbe5da1d3f1971
merged

diff -r f71978e47cd5 -r 7b92238454d6 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon Apr 26 15:14:14 2010 +0200
+++ b/src/Pure/axclass.ML	Mon Apr 26 16:08:04 2010 +0200
@@ -15,7 +15,6 @@
   val prove_arity: string * sort list * sort -> tactic -> theory -> theory
   type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
   val get_info: theory -> class -> info
-  val class_intros: theory -> thm list
   val class_of_param: theory -> string -> class option
   val cert_classrel: theory -> class * class -> class * class
   val read_classrel: theory -> xstring * xstring -> class * class
@@ -166,22 +165,13 @@
 val diff_merge_classrels_of = #diff_merge_classrels o rep_data;
 
 
-(* maintain axclasses *)
+(* axclasses with parameters *)
 
 fun get_info thy c =
   (case Symtab.lookup (axclasses_of thy) c of
     SOME info => info
   | NONE => error ("No such axclass: " ^ quote c));
 
-fun class_intros thy =
-  let
-    fun add_intro c = (case try (get_info thy) c of SOME {intro, ...} => cons intro | _ => I);
-    val classes = Sign.all_classes thy;
-  in map (Thm.class_triv thy) classes @ fold add_intro classes [] end;
-
-
-(* maintain params *)
-
 fun all_params_of thy S =
   let val params = params_of thy;
   in fold (fn (x, c) => if Sign.subsort thy (S, [c]) then cons x else I) params [] end;