# HG changeset patch
# User bulwahn
# Date 1285246216 -7200
# Node ID 51e23b48a20283500ad75e30e51bf2e859e80971
# Parent  b1febbbda458670c9e78613d28d4d8d75913af85
handling TYPE_MATCH error by raising user error message if user gives introduction rules with mismatching types

diff -r b1febbbda458 -r 51e23b48a202 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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