replaced Sign.classes by Sign.all_classes (topologically sorted);
authorwenzelm
Fri Dec 29 17:24:41 2006 +0100 (2006-12-29)
changeset 21931314f9e2a442c
parent 21930 918fb0fb5c72
child 21932 7d592dc078e3
replaced Sign.classes by Sign.all_classes (topologically sorted);
src/HOL/Tools/refute.ML
src/Pure/Tools/codegen_names.ML
src/Pure/axclass.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Fri Dec 29 16:47:49 2006 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Dec 29 17:24:41 2006 +0100
     1.3 @@ -424,7 +424,7 @@
     1.4  		val rec_names = Symtab.fold (append o #rec_names o snd)
     1.5            (DatatypePackage.get_datatypes thy) [];
     1.6  		(* string list *)
     1.7 -		val const_of_class_names = map Logic.const_of_class (Sign.classes thy)
     1.8 +		val const_of_class_names = map Logic.const_of_class (Sign.all_classes 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  *)
     2.1 --- a/src/Pure/Tools/codegen_names.ML	Fri Dec 29 16:47:49 2006 +0100
     2.2 +++ b/src/Pure/Tools/codegen_names.ML	Fri Dec 29 17:24:41 2006 +0100
     2.3 @@ -154,7 +154,7 @@
     2.4      | NONE => error (errmsg x) end;
     2.5  
     2.6  fun thyname_of_class thy =
     2.7 -  thyname_of thy (fn thy => member (op =) (Sign.classes thy))
     2.8 +  thyname_of thy (fn thy => member (op =) (Sign.all_classes thy))
     2.9      (fn class => "thyname_of_class: no such class: " ^ quote class);
    2.10  
    2.11  fun thyname_of_classrel thy =
     3.1 --- a/src/Pure/axclass.ML	Fri Dec 29 16:47:49 2006 +0100
     3.2 +++ b/src/Pure/axclass.ML	Fri Dec 29 17:24:41 2006 +0100
     3.3 @@ -126,7 +126,7 @@
     3.4    let
     3.5      fun add_intro c =
     3.6        (case lookup_def thy c of SOME (AxClass {intro, ...}) => cons intro | _ => I);
     3.7 -    val classes = Sign.classes thy;
     3.8 +    val classes = Sign.all_classes thy;
     3.9    in map (Thm.class_triv thy) classes @ fold add_intro classes [] end;
    3.10  
    3.11