src/HOL/Tools/refute.ML
changeset 18932 66ecb05f92c8
parent 18760 97aaecb84afe
child 19233 77ca20b0ed77
--- a/src/HOL/Tools/refute.ML	Mon Feb 06 20:58:57 2006 +0100
+++ b/src/HOL/Tools/refute.ML	Mon Feb 06 20:58:59 2006 +0100
@@ -424,7 +424,7 @@
 		val rec_names = Symtab.foldl (fn (acc, (_, info)) =>
 			#rec_names info @ acc) ([], DatatypePackage.get_datatypes thy)
 		(* string list *)
-		val const_of_class_names = map Sign.const_of_class (Sign.classes (sign_of thy))
+		val const_of_class_names = map Logic.const_of_class (Sign.classes (sign_of thy))
 		(* given a constant 's' of type 'T', which is a subterm of 't', where  *)
 		(* 't' has a (possibly) more general type, the schematic type          *)
 		(* variables in 't' are instantiated to match the type 'T' (may raise  *)
@@ -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 (Sign.const_of_class class ^ ".axioms_") s) axioms
+						val class_axioms             = List.filter (fn (s, _) => String.isPrefix (Logic.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) =>
@@ -687,7 +687,7 @@
 						(* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" and *)
 						(* the introduction rule "class.intro" as axioms              *)
 						let
-							val class   = Sign.class_of_const s
+							val class   = Logic.class_of_const s
 							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)