src/Tools/code/code_wellsorted.ML

     (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns);
 
 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;
 
 
 (* data structures *)