handling TYPE_MATCH error by raising user error message if user gives introduction rules with mismatching types

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Sep 23 14:50:16 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Sep 23 14:50:16 2010 +0200
@@ -489,6 +489,10 @@
       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)
+            ^ " (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)
         in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end
       fun instantiate_typ th =
         let