src/HOL/Tools/refute.ML
changeset 17274 746bb4c56800
parent 17261 193b84a70ca4
child 17314 04e21a27c0ad
     1.1 --- a/src/HOL/Tools/refute.ML	Tue Sep 06 16:29:39 2005 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Tue Sep 06 16:59:48 2005 +0200
     1.3 @@ -478,7 +478,7 @@
     1.4  					let
     1.5  						(* obtain the axioms generated by the "axclass" command *)
     1.6  						(* (string * Term.term) list *)
     1.7 -						val class_axioms             = List.filter (fn (s, _) => String.isPrefix (class ^ ".axioms_") s) axioms
     1.8 +						val class_axioms             = List.filter (fn (s, _) => String.isPrefix (Sign.const_of_class class ^ ".axioms_") s) axioms
     1.9  						(* replace the one schematic type variable in each axiom by the actual type 'T' *)
    1.10  						(* (string * Term.term) list *)
    1.11  						val monomorphic_class_axioms = map (fn (axname, ax) =>
    1.12 @@ -690,7 +690,7 @@
    1.13  							val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class)
    1.14  							(* Term.term option *)
    1.15  							val ofclass_ax = (SOME (specialize_type ((s, T), inclass)) handle Type.TYPE_MATCH => NONE)
    1.16 -							val intro_ax   = (Option.map (fn t => specialize_type ((s, T), t)) (assoc (axioms, class ^ ".intro")) handle Type.TYPE_MATCH => NONE)
    1.17 +							val intro_ax   = (Option.map (fn t => specialize_type ((s, T), t)) (assoc (axioms, s ^ ".intro")) handle Type.TYPE_MATCH => NONE)
    1.18  							val axs'       = (case ofclass_ax of NONE => axs | SOME ax => if mem_term (ax, axs) then
    1.19  									(* collect relevant type axioms *)
    1.20  									collect_type_axioms (axs, T)
    1.21 @@ -701,7 +701,7 @@
    1.22  									(* collect relevant type axioms *)
    1.23  									collect_type_axioms (axs', T)
    1.24  								else
    1.25 -									(immediate_output (" " ^ class ^ ".intro");
    1.26 +									(immediate_output (" " ^ s ^ ".intro");
    1.27  									collect_term_axioms (ax :: axs', ax)))
    1.28  						in
    1.29  							axs''