# HG changeset patch
# User haftmann
# Date 1151498110 -7200
# Node ID b171fac592bbc50a93b304a587d2b156eb18263b
# Parent  e4c9f6946db341e79119d427556539d67b38cb96
added lookup function for parameters

diff -r e4c9f6946db3 -r b171fac592bb src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Jun 28 09:27:53 2006 +0200
+++ b/src/Pure/axclass.ML	Wed Jun 28 14:35:10 2006 +0200
@@ -12,6 +12,7 @@
   val class_intros: theory -> thm list
   val params_of: theory -> class -> string list
   val all_params_of: theory -> sort -> string list
+  val class_of: theory -> string -> class option
   val print_axclasses: theory -> unit
   val cert_classrel: theory -> class * class -> class * class
   val read_classrel: theory -> xstring * xstring -> class * class
@@ -133,6 +134,9 @@
 fun params_of thy c = get_params thy (fn c' => c' = c);
 fun all_params_of thy S = get_params thy (fn c => Sign.subsort thy (S, [c]));
 
+fun class_of thy =
+  AList.lookup (op =) (#2 (get_axclasses thy));
+
 
 (* maintain instances *)