1.1 --- a/src/Tools/code/code_funcgr.ML	Mon Dec 01 12:17:01 2008 +0100
     1.2 +++ b/src/Tools/code/code_funcgr.ML	Mon Dec 01 12:17:02 2008 +0100
     1.3 @@ -13,9 +13,12 @@
     1.4    val typ: T -> string -> (string * sort) list * typ
     1.5    val all: T -> string list
     1.6    val pretty: theory -> T -> Pretty.T
     1.7 -  val make: theory -> string list -> T
     1.8 -  val eval_conv: theory -> (term -> term * (T -> thm)) -> cterm -> thm
     1.9 -  val eval_term: theory -> (term -> term * (T -> 'a)) -> term -> 'a
    1.10 +  val make: theory -> string list
    1.11 +    -> ((sort -> sort) * Sorts.algebra) * T
    1.12 +  val eval_conv: theory
    1.13 +    -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> thm)) -> cterm -> thm
    1.14 +  val eval_term: theory
    1.15 +    -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a
    1.16    val timing: bool ref
    1.17  end
    1.18  
    1.19 @@ -235,7 +238,7 @@
    1.20      val consts' = consts_of t'';
    1.21      val dicts = instances_of_consts thy algebra funcgr' consts';
    1.22      val funcgr'' = ensure_consts thy algebra dicts funcgr';
    1.23 -  in (evaluator_lift evaluator_funcgr thm funcgr'', funcgr'') end;
    1.24 +  in (evaluator_lift (evaluator_funcgr (Code.operational_algebra thy)) thm funcgr'', funcgr'') end;
    1.25  
    1.26  fun proto_eval_conv thy =
    1.27    let
    1.28 @@ -267,7 +270,8 @@
    1.29  );
    1.30  
    1.31  fun make thy =
    1.32 -  Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);
    1.33 +  pair (Code.operational_algebra thy)
    1.34 +  o Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);
    1.35  
    1.36  fun eval_conv thy f =
    1.37    fst o Funcgr.change_yield thy o proto_eval_conv thy f;
    1.38 @@ -280,7 +284,7 @@
    1.39  
    1.40  fun code_depgr thy consts =
    1.41    let
    1.42 -    val gr = make thy consts;
    1.43 +    val (_, gr) = make thy consts;
    1.44      val select = Graph.all_succs gr consts;
    1.45    in
    1.46      gr