--- 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)
--- 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));