1.1 --- a/src/Tools/code/code_funcgr.ML	Fri Nov 07 08:57:15 2008 +0100
     1.2 +++ b/src/Tools/code/code_funcgr.ML	Mon Nov 10 08:18:56 2008 +0100
     1.3 @@ -14,8 +14,8 @@
     1.4    val all: T -> string list
     1.5    val pretty: theory -> T -> Pretty.T
     1.6    val make: theory -> string list -> T
     1.7 -  val eval_conv: theory -> (term -> term * (T -> term -> thm)) -> cterm -> thm
     1.8 -  val eval_term: theory -> (term -> term * (T -> term -> 'a)) -> term -> 'a
     1.9 +  val eval_conv: theory -> (term -> term * (T -> thm)) -> cterm -> thm
    1.10 +  val eval_term: theory -> (term -> term * (T -> 'a)) -> term -> 'a
    1.11    val timing: bool ref
    1.12  end
    1.13  
    1.14 @@ -218,42 +218,42 @@
    1.15  
    1.16  val ensure_consts = ensure_consts;
    1.17  
    1.18 -fun proto_eval thy cterm_of evaluator_fr evaluator proto_ct funcgr =
    1.19 +fun proto_eval thy cterm_of evaluator_lift evaluator proto_ct funcgr =
    1.20    let
    1.21      val ct = cterm_of proto_ct;
    1.22      val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
    1.23      val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
    1.24 -    fun consts_of t = fold_aterms (fn Const c_ty => cons c_ty | _ => I)
    1.25 -      t [];
    1.26 +    fun consts_of t =
    1.27 +      fold_aterms (fn Const c_ty => cons c_ty | _ => I) t [];
    1.28      val algebra = Code.coregular_algebra thy;
    1.29      val thm = Code.preprocess_conv thy ct;
    1.30      val ct' = Thm.rhs_of thm;
    1.31      val t' = Thm.term_of ct';
    1.32      val consts = map fst (consts_of t');
    1.33      val funcgr' = ensure_consts thy algebra consts funcgr;
    1.34 -    val (t'', evaluator') = apsnd evaluator_fr (evaluator t');
    1.35 +    val (t'', evaluator_funcgr) = evaluator t';
    1.36      val consts' = consts_of t'';
    1.37      val dicts = instances_of_consts thy algebra funcgr' consts';
    1.38      val funcgr'' = ensure_consts thy algebra dicts funcgr';
    1.39 -  in (evaluator' thm funcgr'' t'', funcgr'') end;
    1.40 +  in (evaluator_lift evaluator_funcgr thm funcgr'', funcgr'') end;
    1.41  
    1.42  fun proto_eval_conv thy =
    1.43    let
    1.44 -    fun evaluator evaluator' thm1 funcgr t =
    1.45 +    fun evaluator_lift evaluator thm1 funcgr =
    1.46        let
    1.47 -        val thm2 = evaluator' funcgr t;
    1.48 +        val thm2 = evaluator funcgr;
    1.49          val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
    1.50        in
    1.51          Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
    1.52            error ("could not construct evaluation proof:\n"
    1.53            ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
    1.54        end;
    1.55 -  in proto_eval thy I evaluator end;
    1.56 +  in proto_eval thy I evaluator_lift end;
    1.57  
    1.58  fun proto_eval_term thy =
    1.59    let
    1.60 -    fun evaluator evaluator' _ funcgr t = evaluator' funcgr t;
    1.61 -  in proto_eval thy (Thm.cterm_of thy) evaluator end;
    1.62 +    fun evaluator_lift evaluator _ funcgr = evaluator funcgr;
    1.63 +  in proto_eval thy (Thm.cterm_of thy) evaluator_lift end;
    1.64  
    1.65  end; (*local*)
    1.66