# HG changeset patch
# User wenzelm
# Date 1272390244 -7200
# Node ID 85bc9b7c4d18639deb3b7771361a14447f749fcb
# Parent  cc8db72952495bcc97ef2f460d1b7fb018bd0009
tuned signature;

diff -r cc8db7295249 -r 85bc9b7c4d18 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Apr 27 16:24:57 2010 +0200
+++ b/src/Pure/axclass.ML	Tue Apr 27 19:44:04 2010 +0200
@@ -7,35 +7,35 @@
 
 signature AX_CLASS =
 sig
-  val define_class: binding * class list -> string list ->
-    (Thm.binding * term list) list -> theory -> class * theory
+  type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
+  val get_info: theory -> class -> info
+  val class_of_param: theory -> string -> class option
+  val instance_name: string * class -> string
+  val thynames_of_arity: theory -> class * string -> string list
+  val param_of_inst: theory -> string * string -> string
+  val inst_of_param: theory -> string -> (string * string) option
+  val unoverload: theory -> thm -> thm
+  val overload: theory -> thm -> thm
+  val unoverload_conv: theory -> conv
+  val overload_conv: theory -> conv
+  val lookup_inst_param: Consts.T -> ((string * string) * 'a) list -> string * typ -> 'a option
+  val unoverload_const: theory -> string * typ -> string
+  val cert_classrel: theory -> class * class -> class * class
+  val read_classrel: theory -> xstring * xstring -> class * class
+  val declare_overloaded: string * typ -> theory -> term * theory
+  val define_overloaded: binding -> string * term -> theory -> thm * theory
   val add_classrel: thm -> theory -> theory
   val add_arity: thm -> theory -> theory
   val prove_classrel: class * class -> tactic -> theory -> theory
   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_of_param: theory -> string -> class option
-  val cert_classrel: theory -> class * class -> class * class
-  val read_classrel: theory -> xstring * xstring -> class * class
+  val define_class: binding * class list -> string list ->
+    (Thm.binding * term list) list -> theory -> class * theory
   val axiomatize_class: binding * class list -> theory -> theory
   val axiomatize_class_cmd: binding * xstring list -> theory -> theory
   val axiomatize_classrel: (class * class) list -> theory -> theory
   val axiomatize_classrel_cmd: (xstring * xstring) list -> theory -> theory
   val axiomatize_arity: arity -> theory -> theory
   val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
-  val instance_name: string * class -> string
-  val declare_overloaded: string * typ -> theory -> term * theory
-  val define_overloaded: binding -> string * term -> theory -> thm * theory
-  val unoverload: theory -> thm -> thm
-  val overload: theory -> thm -> thm
-  val unoverload_conv: theory -> conv
-  val overload_conv: theory -> conv
-  val unoverload_const: theory -> string * typ -> string
-  val lookup_inst_param: Consts.T -> ((string * string) * 'a) list -> string * typ -> 'a option
-  val param_of_inst: theory -> string * string -> string
-  val inst_of_param: theory -> string -> (string * string) option
-  val thynames_of_arity: theory -> class * string -> string list
 end;
 
 structure AxClass: AX_CLASS =