diff -r 36a011423fcc -r 11001968caae src/Tools/code/code_wellsorted.ML
--- a/src/Tools/code/code_wellsorted.ML	Mon May 11 09:40:38 2009 +0200
+++ b/src/Tools/code/code_wellsorted.ML	Mon May 11 09:40:39 2009 +0200
@@ -64,7 +64,7 @@
 fun tyscm_rhss_of thy c eqns =
   let
     val tyscm = case eqns of [] => Code.default_typscheme thy c
-      | ((thm, _) :: _) => (snd o Code_Unit.head_eqn thy) thm;
+      | ((thm, _) :: _) => Code_Unit.typscheme_eqn thy thm;
     val rhss = consts_of thy eqns;
   in (tyscm, rhss) end;