# HG changeset patch
# User haftmann
# Date 1166038700 -3600
# Node ID b2cbcf8a018e0efa238333ce2b3299506abfb613
# Parent  84fd5de0691c02fc9b657272f4bb164c78bcfba9
cleanup

diff -r 84fd5de0691c -r b2cbcf8a018e src/HOL/ex/CodeEval.thy
--- 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;
 *}
 
diff -r 84fd5de0691c -r b2cbcf8a018e src/Pure/codegen.ML
--- 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