# 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;