src/Tools/code/code_funcgr.ML

   type T
   val eqns: T -> string -> (thm * bool) list
   val typ: T -> string -> (string * sort) list * typ
   val all: T -> string list
   val pretty: theory -> T -> Pretty.T
-  val make: theory -> string list -> T
-  val eval_conv: theory -> (term -> term * (T -> thm)) -> cterm -> thm
-  val eval_term: theory -> (term -> term * (T -> 'a)) -> term -> 'a
+  val make: theory -> string list
+    -> ((sort -> sort) * Sorts.algebra) * T
+  val eval_conv: theory
+    -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> thm)) -> cterm -> thm
+  val eval_term: theory
+    -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a
   val timing: bool ref
 end
 
 structure Code_Funcgr : CODE_FUNCGR =
 struct

     val funcgr' = ensure_consts thy algebra consts funcgr;
     val (t'', evaluator_funcgr) = evaluator t';
     val consts' = consts_of t'';
     val dicts = instances_of_consts thy algebra funcgr' consts';
     val funcgr'' = ensure_consts thy algebra dicts funcgr';
-  in (evaluator_lift evaluator_funcgr thm funcgr'', funcgr'') end;
+  in (evaluator_lift (evaluator_funcgr (Code.operational_algebra thy)) thm funcgr'', funcgr'') end;
 
 fun proto_eval_conv thy =
   let
     fun evaluator_lift evaluator thm1 funcgr =
       let

     Graph.del_nodes ((Graph.all_preds funcgr 
       o filter (can (Graph.get_node funcgr))) cs) funcgr;
 );
 
 fun make thy =
-  Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);
+  pair (Code.operational_algebra thy)
+  o Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);
 
 fun eval_conv thy f =
   fst o Funcgr.change_yield thy o proto_eval_conv thy f;
 
 fun eval_term thy f =

 
 (** diagnostic commands **)
 
 fun code_depgr thy consts =
   let
-    val gr = make thy consts;
+    val (_, gr) = make thy consts;
     val select = Graph.all_succs gr consts;
   in
     gr
     |> not (null consts) ? Graph.subgraph (member (op =) select) 
     |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))