--- a/src/HOL/ex/CodeEval.thy Wed Dec 13 20:38:19 2006 +0100
+++ b/src/HOL/ex/CodeEval.thy Wed Dec 13 20:38:20 2006 +0100
@@ -8,8 +8,6 @@
imports CodeEmbed
begin
-section {* A simple embedded term evaluation mechanism *}
-
subsection {* The typ_of class *}
class typ_of =
@@ -139,8 +137,6 @@
val t = eval_term thy (Sign.read_term thy t);
in (writeln o Sign.string_of_term thy) t end;
-exception Eval of term;
-
end;
*}
--- a/src/Pure/codegen.ML Wed Dec 13 20:38:19 2006 +0100
+++ b/src/Pure/codegen.ML Wed Dec 13 20:38:20 2006 +0100
@@ -332,9 +332,9 @@
modules = modules, test_params = test_params} thy
end;
-fun preprocess thy ths =
+fun preprocess thy =
let val {preprocs, ...} = CodegenData.get thy
- in Library.foldl (fn (ths, (_, f)) => f thy ths) (ths, preprocs) end;
+ in fold (fn (_, f) => f thy) preprocs end;
fun preprocess_term thy t =
let