# HG changeset patch
# User haftmann
# Date 1235322141 -3600
# Node ID c95e8f696b6839dad83ef6a0110d891c116da467
# Parent  672012330c4eba51ec3cbbb5ee3ae61c57178c87
clarified status of variables in evaluation terms; tuned header

diff -r 672012330c4e -r c95e8f696b68 src/Tools/code/code_wellsorted.ML
--- 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