src/Tools/code/code_wellsorted.ML

 (*  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.
 *)
 
 signature CODE_FUNCGR =
 sig

     val t' = Thm.term_of ct';
     val (t'', evaluator_eqngr) = evaluator t';
     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
     (evaluator_lift (evaluator_eqngr algebra') thm (snd arities_eqngr'),
       arities_eqngr')