--- a/src/Tools/code/code_wellsorted.ML Sun Feb 22 18:00:05 2009 +0100
+++ b/src/Tools/code/code_wellsorted.ML Sun Feb 22 18:02:21 2009 +0100
@@ -1,7 +1,7 @@
(* Title: Tools/code/code_wellsorted.ML
Author: Florian Haftmann, TU Muenchen
-Retrieving, well-sorting and structuring code equations in graph
+Producing well-sorted systems of code equations in a graph
with explicit dependencies -- the Waisenhaus algorithm.
*)
@@ -301,7 +301,7 @@
val consts = map fst (consts_of t');
val consts' = consts_of t'';
val const_matches' = fold (fn (c, ty) =>
- insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty))) consts' [];
+ insert (op =) (c, Sign.const_typargs thy (c, ty))) consts' [];
val (algebra', arities_eqngr') =
extend_arities_eqngr thy consts const_matches' arities_eqngr;
in