--- a/src/Pure/Tools/codegen_func.ML Tue Jun 05 15:16:09 2007 +0200
+++ b/src/Pure/Tools/codegen_func.ML Tue Jun 05 15:16:10 2007 +0200
@@ -42,7 +42,7 @@
val thy = Thm.theory_of_thm thm;
val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm)
- handle THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
+ | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
fun vars_of t = fold_aterms
(fn Var (v, _) => insert (op =) v
| Free _ => bad_thm ("Illegal free variable in rewrite theorem\n"