# HG changeset patch
# User haftmann
# Date 1181049370 -7200
# Node ID 9ef65be6bb2a7206e68464b52b2d97b54c31386a
# Parent  ef04b4c12593157a7fdaacfcb3439dc337d29f7d
fixed broken execption handling

diff -r ef04b4c12593 -r 9ef65be6bb2a src/Pure/Tools/codegen_func.ML
--- 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"