1.1 --- a/src/Tools/Code/code_thingol.ML	Tue Dec 21 15:15:55 2010 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Dec 21 15:15:55 2010 +0100
     1.3 @@ -912,31 +912,37 @@
     1.4  fun dynamic_value thy postproc evaluator =
     1.5    Code_Preproc.dynamic_value thy postproc (dynamic_evaluator thy evaluator);
     1.6  
     1.7 -fun provide_program thy consts f algebra eqngr =
     1.8 +fun lift_evaluation thy evaluation' algebra eqngr naming program vs t =
     1.9 +  let
    1.10 +    val (((_, program'), (((vs', ty'), t'), deps)), _) =
    1.11 +      ensure_value thy algebra eqngr t (NONE, (naming, program));
    1.12 +  in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end;
    1.13 +
    1.14 +fun lift_evaluator thy evaluator' consts algebra eqngr =
    1.15    let
    1.16      fun generate_consts thy algebra eqngr =
    1.17        fold_map (ensure_const thy algebra eqngr false);
    1.18 -    val (consts', (naming, program)) = invoke_generation true thy (algebra, eqngr)
    1.19 -      generate_consts consts;
    1.20 -  in f algebra eqngr naming program consts' end;
    1.21 +    val (consts', (naming, program)) =
    1.22 +      invoke_generation true thy (algebra, eqngr) generate_consts consts;
    1.23 +    val evaluation' = evaluator' naming program consts';
    1.24 +  in lift_evaluation thy evaluation' algebra eqngr naming program end;
    1.25  
    1.26 -fun static_evaluation thy evaluator algebra eqngr naming program consts' vs t =
    1.27 +fun lift_evaluator_simple thy evaluator' consts algebra eqngr =
    1.28    let
    1.29 -    val (((_, program'), (((vs', ty'), t'), deps)), _) =
    1.30 -      ensure_value thy algebra eqngr t (NONE, (naming, program));
    1.31 -  in evaluator naming program' consts' ((original_sorts vs vs', (vs', ty')), t') deps end;
    1.32 +    fun generate_consts thy algebra eqngr =
    1.33 +      fold_map (ensure_const thy algebra eqngr false);
    1.34 +    val (consts', (naming, program)) =
    1.35 +      invoke_generation true thy (algebra, eqngr) generate_consts consts;
    1.36 +  in evaluator' program end;
    1.37  
    1.38  fun static_conv thy consts conv =
    1.39 -  Code_Preproc.static_conv thy consts
    1.40 -    (provide_program thy consts (static_evaluation thy conv));
    1.41 +  Code_Preproc.static_conv thy consts (lift_evaluator thy conv consts);
    1.42  
    1.43  fun static_conv_simple thy consts conv =
    1.44 -  Code_Preproc.static_conv thy consts
    1.45 -    (provide_program thy consts (fn _ => fn _ => fn _ => fn program => fn _ => conv program));
    1.46 +  Code_Preproc.static_conv thy consts (lift_evaluator_simple thy conv consts);
    1.47  
    1.48  fun static_value thy postproc consts evaluator =
    1.49 -  Code_Preproc.static_value thy postproc consts
    1.50 -    (provide_program thy consts (static_evaluation thy evaluator));
    1.51 +  Code_Preproc.static_value thy postproc consts (lift_evaluator thy evaluator consts);
    1.52  
    1.53  
    1.54  (** diagnostic commands **)