1.1 --- a/src/Tools/code/code_wellsorted.ML	Mon Mar 02 16:58:39 2009 +0100
     1.2 +++ b/src/Tools/code/code_wellsorted.ML	Mon Mar 02 16:58:39 2009 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  with explicit dependencies -- the Waisenhaus algorithm.
     1.5  *)
     1.6  
     1.7 -signature CODE_FUNCGR =
     1.8 +signature CODE_WELLSORTED =
     1.9  sig
    1.10    type T
    1.11    val eqns: T -> string -> (thm * bool) list
    1.12 @@ -20,7 +20,7 @@
    1.13      -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a
    1.14  end
    1.15  
    1.16 -structure Code_Funcgr : CODE_FUNCGR =
    1.17 +structure Code_Wellsorted : CODE_WELLSORTED =
    1.18  struct
    1.19  
    1.20  (** the equation graph type **)