--- a/src/HOL/Tools/refute.ML Tue Sep 06 16:29:39 2005 +0200
+++ b/src/HOL/Tools/refute.ML Tue Sep 06 16:59:48 2005 +0200
@@ -478,7 +478,7 @@
let
(* obtain the axioms generated by the "axclass" command *)
(* (string * Term.term) list *)
- val class_axioms = List.filter (fn (s, _) => String.isPrefix (class ^ ".axioms_") s) axioms
+ val class_axioms = List.filter (fn (s, _) => String.isPrefix (Sign.const_of_class class ^ ".axioms_") s) axioms
(* replace the one schematic type variable in each axiom by the actual type 'T' *)
(* (string * Term.term) list *)
val monomorphic_class_axioms = map (fn (axname, ax) =>
@@ -690,7 +690,7 @@
val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class)
(* Term.term option *)
val ofclass_ax = (SOME (specialize_type ((s, T), inclass)) handle Type.TYPE_MATCH => NONE)
- val intro_ax = (Option.map (fn t => specialize_type ((s, T), t)) (assoc (axioms, class ^ ".intro")) handle Type.TYPE_MATCH => NONE)
+ val intro_ax = (Option.map (fn t => specialize_type ((s, T), t)) (assoc (axioms, s ^ ".intro")) handle Type.TYPE_MATCH => NONE)
val axs' = (case ofclass_ax of NONE => axs | SOME ax => if mem_term (ax, axs) then
(* collect relevant type axioms *)
collect_type_axioms (axs, T)
@@ -701,7 +701,7 @@
(* collect relevant type axioms *)
collect_type_axioms (axs', T)
else
- (immediate_output (" " ^ class ^ ".intro");
+ (immediate_output (" " ^ s ^ ".intro");
collect_term_axioms (ax :: axs', ax)))
in
axs''