src/Tools/Code/code_thingol.ML
changeset 32123 8bac9ee4b28d
parent 31962 baa8dce5bc45
child 32131 7913823f14e3
     1.1 --- a/src/Tools/Code/code_thingol.ML	Tue Jul 21 15:44:31 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Jul 21 15:44:31 2009 +0200
     1.3 @@ -82,10 +82,10 @@
     1.4    val read_const_exprs: theory -> string list -> string list * string list
     1.5    val consts_program: theory -> string list -> string list * (naming * program)
     1.6    val cached_program: theory -> naming * program
     1.7 -  val eval_conv: theory -> (sort -> sort)
     1.8 +  val eval_conv: theory
     1.9      -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> cterm -> thm)
    1.10      -> cterm -> thm
    1.11 -  val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a)
    1.12 +  val eval: theory -> ((term -> term) -> 'a -> 'a)
    1.13      -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
    1.14      -> term -> 'a
    1.15  end;
    1.16 @@ -803,8 +803,8 @@
    1.17      val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
    1.18    in evaluator naming program ((vs'', (vs', ty')), t') deps end;
    1.19  
    1.20 -fun eval_conv thy prep_sort = Code_Preproc.eval_conv thy prep_sort o base_evaluator thy;
    1.21 -fun eval thy prep_sort postproc = Code_Preproc.eval thy prep_sort postproc o base_evaluator thy;
    1.22 +fun eval_conv thy = Code_Preproc.eval_conv thy o base_evaluator thy;
    1.23 +fun eval thy postproc = Code_Preproc.eval thy postproc o base_evaluator thy;
    1.24  
    1.25  
    1.26  (** diagnostic commands **)