# HG changeset patch
# User wenzelm
# Date 1139255939 -3600
# Node ID 66ecb05f92c8cd754cd2adf7d4946a225fb3be1c
# Parent  427df66052a1b510b4094e06e023e57546ef1d1d
Logic.const_of_class/class_of_const;

diff -r 427df66052a1 -r 66ecb05f92c8 src/HOL/Tools/refute.ML
--- 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)
diff -r 427df66052a1 -r 66ecb05f92c8 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon Feb 06 20:58:57 2006 +0100
+++ b/src/Pure/axclass.ML	Mon Feb 06 20:58:59 2006 +0100
@@ -200,7 +200,7 @@
     (*declare axioms and rule*)
     val (([intro], [axioms]), axms_thy) =
       class_thy
-      |> Theory.add_path (Sign.const_of_class bclass)
+      |> Theory.add_path (Logic.const_of_class bclass)
       |> PureThy.add_axioms_i [Thm.no_attributes (introN, intro_axm)]
       ||>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)];
     val info = {super_classes = super_classes, intro = intro, axioms = axioms};
@@ -208,7 +208,7 @@
     (*store info*)
     val (_, final_thy) =
       axms_thy
-      |> Theory.add_finals_i false [Const (Sign.const_of_class class, a_itselfT --> propT)]
+      |> Theory.add_finals_i false [Const (Logic.const_of_class class, a_itselfT --> propT)]
       |> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts)
       ||> Theory.restore_naming class_thy
       ||> AxclassesData.map (Symtab.update (class, info));