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;
 *}