# HG changeset patch
# User wenzelm
# Date 1191942638 -7200
# Node ID 3419943838f549472cc49f57de4855eac8602b7d
# Parent  48e08f37ce924cedefdf921285a848dd9e69e2d8
renamed AxClass.get_definition to AxClass.get_info (again);

diff -r 48e08f37ce92 -r 3419943838f5 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Tue Oct 09 17:10:36 2007 +0200
+++ b/src/HOL/Tools/refute.ML	Tue Oct 09 17:10:38 2007 +0200
@@ -794,7 +794,7 @@
       val superclasses = distinct (op =) superclasses
       val class_axioms = maps (fn class => map (fn ax =>
         ("<" ^ class ^ ">", Thm.prop_of ax))
-        (#axioms (AxClass.get_definition thy class) handle ERROR _ => []))
+        (#axioms (AxClass.get_info thy class) handle ERROR _ => []))
         superclasses
       (* replace the (at most one) schematic type variable in each axiom *)
       (* by the actual type 'T'                                          *)
diff -r 48e08f37ce92 -r 3419943838f5 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Oct 09 17:10:36 2007 +0200
+++ b/src/Pure/Isar/code.ML	Tue Oct 09 17:10:38 2007 +0200
@@ -597,7 +597,7 @@
 fun operational_algebra thy =
   let
     fun add_iff_operational class =
-      can (AxClass.get_definition thy) class ? cons class;
+      can (AxClass.get_info thy) class ? cons class;
     val operational_classes = fold add_iff_operational (Sign.all_classes thy) []
   in retrieve_algebra thy (member (op =) operational_classes) end;
 
diff -r 48e08f37ce92 -r 3419943838f5 src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Tue Oct 09 17:10:36 2007 +0200
+++ b/src/Tools/code/code_target.ML	Tue Oct 09 17:10:38 2007 +0200
@@ -1903,13 +1903,13 @@
 
 fun cert_class thy class =
   let
-    val _ = AxClass.get_definition thy class;
+    val _ = AxClass.get_info thy class;
   in class end;
 
 fun read_class thy raw_class =
   let
     val class = Sign.intern_class thy raw_class;
-    val _ = AxClass.get_definition thy class;
+    val _ = AxClass.get_info thy class;
   in class end;
 
 fun cert_tyco thy tyco =