Logic.const_of_class/class_of_const;
authorwenzelm
Mon Feb 06 20:58:59 2006 +0100 (2006-02-06)
changeset 1893266ecb05f92c8
parent 18931 427df66052a1
child 18933 057b32b8f1fd
Logic.const_of_class/class_of_const;
src/HOL/Tools/refute.ML
src/Pure/axclass.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Mon Feb 06 20:58:57 2006 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Mon Feb 06 20:58:59 2006 +0100
     1.3 @@ -424,7 +424,7 @@
     1.4  		val rec_names = Symtab.foldl (fn (acc, (_, info)) =>
     1.5  			#rec_names info @ acc) ([], DatatypePackage.get_datatypes thy)
     1.6  		(* string list *)
     1.7 -		val const_of_class_names = map Sign.const_of_class (Sign.classes (sign_of thy))
     1.8 +		val const_of_class_names = map Logic.const_of_class (Sign.classes (sign_of thy))
     1.9  		(* given a constant 's' of type 'T', which is a subterm of 't', where  *)
    1.10  		(* 't' has a (possibly) more general type, the schematic type          *)
    1.11  		(* variables in 't' are instantiated to match the type 'T' (may raise  *)
    1.12 @@ -478,7 +478,7 @@
    1.13  					let
    1.14  						(* obtain the axioms generated by the "axclass" command *)
    1.15  						(* (string * Term.term) list *)
    1.16 -						val class_axioms             = List.filter (fn (s, _) => String.isPrefix (Sign.const_of_class class ^ ".axioms_") s) axioms
    1.17 +						val class_axioms             = List.filter (fn (s, _) => String.isPrefix (Logic.const_of_class class ^ ".axioms_") s) axioms
    1.18  						(* replace the one schematic type variable in each axiom by the actual type 'T' *)
    1.19  						(* (string * Term.term) list *)
    1.20  						val monomorphic_class_axioms = map (fn (axname, ax) =>
    1.21 @@ -687,7 +687,7 @@
    1.22  						(* axiomatic type classes: add "OFCLASS(?'a::c, c_class)" and *)
    1.23  						(* the introduction rule "class.intro" as axioms              *)
    1.24  						let
    1.25 -							val class   = Sign.class_of_const s
    1.26 +							val class   = Logic.class_of_const s
    1.27  							val inclass = Logic.mk_inclass (TVar (("'a", 0), [class]), class)
    1.28  							(* Term.term option *)
    1.29  							val ofclass_ax = (SOME (specialize_type ((s, T), inclass)) handle Type.TYPE_MATCH => NONE)
     2.1 --- a/src/Pure/axclass.ML	Mon Feb 06 20:58:57 2006 +0100
     2.2 +++ b/src/Pure/axclass.ML	Mon Feb 06 20:58:59 2006 +0100
     2.3 @@ -200,7 +200,7 @@
     2.4      (*declare axioms and rule*)
     2.5      val (([intro], [axioms]), axms_thy) =
     2.6        class_thy
     2.7 -      |> Theory.add_path (Sign.const_of_class bclass)
     2.8 +      |> Theory.add_path (Logic.const_of_class bclass)
     2.9        |> PureThy.add_axioms_i [Thm.no_attributes (introN, intro_axm)]
    2.10        ||>> PureThy.add_axiomss_i [Thm.no_attributes (axiomsN, abs_axms)];
    2.11      val info = {super_classes = super_classes, intro = intro, axioms = axioms};
    2.12 @@ -208,7 +208,7 @@
    2.13      (*store info*)
    2.14      val (_, final_thy) =
    2.15        axms_thy
    2.16 -      |> Theory.add_finals_i false [Const (Sign.const_of_class class, a_itselfT --> propT)]
    2.17 +      |> Theory.add_finals_i false [Const (Logic.const_of_class class, a_itselfT --> propT)]
    2.18        |> PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts)
    2.19        ||> Theory.restore_naming class_thy
    2.20        ||> AxclassesData.map (Symtab.update (class, info));