renamed AxClass.get_definition to AxClass.get_info (again);
authorwenzelm
Tue Oct 09 17:10:38 2007 +0200 (2007-10-09)
changeset 249283419943838f5
parent 24927 48e08f37ce92
child 24929 408becab067e
renamed AxClass.get_definition to AxClass.get_info (again);
src/HOL/Tools/refute.ML
src/Pure/Isar/code.ML
src/Tools/code/code_target.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Tue Oct 09 17:10:36 2007 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Tue Oct 09 17:10:38 2007 +0200
     1.3 @@ -794,7 +794,7 @@
     1.4        val superclasses = distinct (op =) superclasses
     1.5        val class_axioms = maps (fn class => map (fn ax =>
     1.6          ("<" ^ class ^ ">", Thm.prop_of ax))
     1.7 -        (#axioms (AxClass.get_definition thy class) handle ERROR _ => []))
     1.8 +        (#axioms (AxClass.get_info thy class) handle ERROR _ => []))
     1.9          superclasses
    1.10        (* replace the (at most one) schematic type variable in each axiom *)
    1.11        (* by the actual type 'T'                                          *)
     2.1 --- a/src/Pure/Isar/code.ML	Tue Oct 09 17:10:36 2007 +0200
     2.2 +++ b/src/Pure/Isar/code.ML	Tue Oct 09 17:10:38 2007 +0200
     2.3 @@ -597,7 +597,7 @@
     2.4  fun operational_algebra thy =
     2.5    let
     2.6      fun add_iff_operational class =
     2.7 -      can (AxClass.get_definition thy) class ? cons class;
     2.8 +      can (AxClass.get_info thy) class ? cons class;
     2.9      val operational_classes = fold add_iff_operational (Sign.all_classes thy) []
    2.10    in retrieve_algebra thy (member (op =) operational_classes) end;
    2.11  
     3.1 --- a/src/Tools/code/code_target.ML	Tue Oct 09 17:10:36 2007 +0200
     3.2 +++ b/src/Tools/code/code_target.ML	Tue Oct 09 17:10:38 2007 +0200
     3.3 @@ -1903,13 +1903,13 @@
     3.4  
     3.5  fun cert_class thy class =
     3.6    let
     3.7 -    val _ = AxClass.get_definition thy class;
     3.8 +    val _ = AxClass.get_info thy class;
     3.9    in class end;
    3.10  
    3.11  fun read_class thy raw_class =
    3.12    let
    3.13      val class = Sign.intern_class thy raw_class;
    3.14 -    val _ = AxClass.get_definition thy class;
    3.15 +    val _ = AxClass.get_info thy class;
    3.16    in class end;
    3.17  
    3.18  fun cert_tyco thy tyco =