src/Pure/axclass.ML
changeset 36346 5518de23101d
parent 36330 0584e203960e
child 36417 54bc1a44967d
     1.1 --- a/src/Pure/axclass.ML	Mon Apr 26 11:20:18 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Mon Apr 26 14:44:41 2010 +0200
     1.3 @@ -15,7 +15,6 @@
     1.4    val prove_arity: string * sort list * sort -> tactic -> theory -> theory
     1.5    type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
     1.6    val get_info: theory -> class -> info
     1.7 -  val class_intros: theory -> thm list
     1.8    val class_of_param: theory -> string -> class option
     1.9    val cert_classrel: theory -> class * class -> class * class
    1.10    val read_classrel: theory -> xstring * xstring -> class * class
    1.11 @@ -166,22 +165,13 @@
    1.12  val diff_merge_classrels_of = #diff_merge_classrels o rep_data;
    1.13  
    1.14  
    1.15 -(* maintain axclasses *)
    1.16 +(* axclasses with parameters *)
    1.17  
    1.18  fun get_info thy c =
    1.19    (case Symtab.lookup (axclasses_of thy) c of
    1.20      SOME info => info
    1.21    | NONE => error ("No such axclass: " ^ quote c));
    1.22  
    1.23 -fun class_intros thy =
    1.24 -  let
    1.25 -    fun add_intro c = (case try (get_info thy) c of SOME {intro, ...} => cons intro | _ => I);
    1.26 -    val classes = Sign.all_classes thy;
    1.27 -  in map (Thm.class_triv thy) classes @ fold add_intro classes [] end;
    1.28 -
    1.29 -
    1.30 -(* maintain params *)
    1.31 -
    1.32  fun all_params_of thy S =
    1.33    let val params = params_of thy;
    1.34    in fold (fn (x, c) => if Sign.subsort thy (S, [c]) then cons x else I) params [] end;