# HG changeset patch
# User wenzelm
# Date 1285335030 -7200
# Node ID d8071cddb8779f46919b9517e8afafc80be5c029
# Parent  6814630157b9afa87aa046e602825f25e2107434
actually handle Type.TYPE_MATCH, not arbitrary exceptions;

diff -r 6814630157b9 -r d8071cddb877 src/HOL/Matrix/Compute_Oracle/linker.ML
--- a/src/HOL/Matrix/Compute_Oracle/linker.ML	Fri Sep 24 15:14:55 2010 +0200
+++ b/src/HOL/Matrix/Compute_Oracle/linker.ML	Fri Sep 24 15:30:30 2010 +0200
@@ -166,7 +166,7 @@
                               else case Consttab.lookup insttab constant of
                                        SOME _ => instantiations
                                      | NONE => ((constant', (constant, Sign.typ_match thy (ty', ty) empty_subst))::instantiations
-                                                handle TYPE_MATCH => instantiations))
+                                                handle Type.TYPE_MATCH => instantiations))
                           ctab instantiations
         val instantiations = fold calc_instantiations cs []
         (*val _ = writeln ("instantiations = "^(makestring (length instantiations)))*)
diff -r 6814630157b9 -r d8071cddb877 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 24 15:14:55 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 24 15:30:30 2010 +0200
@@ -491,7 +491,7 @@
       fun subst_of (pred', pred) =
         let
           val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
-            handle TYPE_MATCH => error ("Type mismatch of predicate " ^ fst (dest_Const pred)
+            handle Type.TYPE_MATCH => error ("Type mismatch of predicate " ^ fst (dest_Const pred)
             ^ " (trying to match " ^ Syntax.string_of_typ ctxt (fastype_of pred')
             ^ " and " ^ Syntax.string_of_typ ctxt (fastype_of pred) ^ ")"
             ^ " in " ^ Display.string_of_thm ctxt th)