--- a/src/HOL/Library/refute.ML Wed Apr 10 13:10:38 2013 +0200
+++ b/src/HOL/Library/refute.ML Wed Apr 10 15:30:19 2013 +0200
@@ -695,7 +695,7 @@
val superclasses = distinct (op =) superclasses
val class_axioms = maps (fn class => map (fn ax =>
("<" ^ class ^ ">", Thm.prop_of ax))
- (#axioms (AxClass.get_info 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' *)