src/Tools/Code/code_preproc.ML

   val print_codeproc: theory -> unit
 
   type code_algebra
   type code_graph
   val eqns: code_graph -> string -> (thm * bool) list
-  val typ: code_graph -> string -> (string * sort) list * typ
+  val sortargs: code_graph -> string -> sort list
   val all: code_graph -> string list
   val pretty: theory -> code_graph -> Pretty.T
   val obtain: theory -> string list -> term list -> code_algebra * code_graph
   val eval_conv: theory
     -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm

 (
   type T = thmproc;
   val empty = make_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []);
   fun copy spec = spec;
   val extend = copy;
-  fun merge pp = merge_thmproc;
+  fun merge _ = merge_thmproc;
 );
 
 fun the_thmproc thy = case Code_Preproc_Data.get thy
  of Thmproc x => x;
 

 
 
 (** sort algebra and code equation graph types **)
 
 type code_algebra = (sort -> sort) * Sorts.algebra;
-type code_graph = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
+type code_graph = ((string * sort) list * (thm * bool) list) Graph.T;
 
 fun eqns eqngr = these o Option.map snd o try (Graph.get_node eqngr);
-fun typ eqngr = fst o Graph.get_node eqngr;
+fun sortargs eqngr = map snd o fst o Graph.get_node eqngr
 fun all eqngr = Graph.keys eqngr;
 
 fun pretty thy eqngr =
   AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
   |> (map o apfst) (Code.string_of_const thy)

 
 fun inst_params thy tyco =
   map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
     o maps (#params o AxClass.get_info thy);
 
+fun typscheme_rhss thy c eqns =
+  let
+    val tyscm = Code.typscheme_eqns thy c (map fst eqns);
+    val rhss = [] |> (fold o fold o fold_aterms)
+      (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
+        (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns);
+  in (tyscm, rhss) end;
+
 
 (* data structures *)
 
 datatype const = Fun of string | Inst of class * string;
 

 
 (* retrieving equations and instances from the background context *)
 
 fun obtain_eqns thy eqngr c =
   case try (Graph.get_node eqngr) c
-   of SOME ((lhs, _), eqns) => ((lhs, []), [])
+   of SOME (lhs, eqns) => ((lhs, []), [])
     | NONE => let
         val eqns = Code.these_eqns thy c
           |> preprocess thy c;
-        val ((lhs, _), rhss) = Code.typscheme_rhss_eqns thy c (map fst eqns);
+        val ((lhs, _), rhss) = typscheme_rhss thy c eqns;
       in ((lhs, rhss), eqns) end;
 
 fun obtain_instance thy arities (inst as (class, tyco)) =
   case AList.lookup (op =) arities inst
    of SOME classess => (classess, ([], []))

       (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
     val inst_tab = Vartab.empty |> fold (fn (v, sort) =>
       Vartab.update ((v, 0), sort)) lhs;
     val eqns = proto_eqns
       |> (map o apfst) (inst_thm thy inst_tab);
-    val (tyscm, rhss') = Code.typscheme_rhss_eqns thy c (map fst eqns);
-    val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr;
+    val ((vs, _), rhss') = typscheme_rhss thy c eqns;
+    val eqngr' = Graph.new_node (c, (vs, eqns)) eqngr;
   in (map (pair c) rhss' @ rhss, eqngr') end;
 
-fun extend_arities_eqngr thy cs ts (arities, eqngr) =
+fun extend_arities_eqngr thy cs ts (arities, (eqngr : code_graph)) =
   let
     val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) =>
       insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts [];
     val (vardeps, (eqntab, insts)) = empty_vardeps_data
       |> fold (ensure_fun thy arities eqngr) cs

     val pp = Syntax.pp_global thy;
     val algebra = Sorts.subalgebra pp (is_proper_class thy)
       (AList.lookup (op =) arities') (Sign.classes_of thy);
     val (rhss, eqngr') = Symtab.fold (add_eqs thy vardeps) eqntab ([], eqngr);
     fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
-      (rhs ~~ (map snd o fst o fst o Graph.get_node eqngr') c);
+      (rhs ~~ sortargs eqngr' c);
     val eqngr'' = fold (fn (c, rhs) => fold
       (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
   in (algebra, (arities', eqngr'')) end;