merged

--- a/src/HOL/Tools/SMT/smt_builtin.ML	Wed Nov 24 16:15:15 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Wed Nov 24 16:51:13 2010 +0100
@@ -9,8 +9,8 @@
 
 signature SMT_BUILTIN =
 sig
+  val is_builtin: Proof.context -> string * typ -> bool
   val is_partially_builtin: Proof.context -> string * typ -> bool
-  val is_builtin: Proof.context -> string * typ -> bool
 end
 
 structure SMT_Builtin: SMT_BUILTIN =
@@ -109,8 +109,8 @@
     SOME proper_type => proper_type T
   | NONE => false)
 
-fun is_partially_builtin _ = lookup_builtin builtins
+fun is_builtin _ = lookup_builtin builtins
 
-fun is_builtin _ = lookup_builtin all_builtins
+fun is_partially_builtin _ = lookup_builtin all_builtins
 
 end

--- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 24 16:15:15 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Nov 24 16:51:13 2010 +0100
@@ -35,6 +35,26 @@
 
 
 
+(* instantiate elimination rules *)
+ 
+local
+  val (cpfalse, cfalse) = `U.mk_cprop (Thm.cterm_of @{theory} @{const False})
+
+  fun inst f ct thm =
+    let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
+    in Thm.instantiate ([], [(cv, ct)]) thm end
+in
+
+fun instantiate_elim thm =
+  (case Thm.concl_of thm of
+    @{const Trueprop} $ Var (_, @{typ bool}) => inst Thm.dest_arg cfalse thm
+  | Var _ => inst I cpfalse thm
+  | _ => thm)
+
+end
+
+
+
 (* simplification of trivial distincts (distinct should have at least
    three elements in the argument list) *)
 
@@ -243,7 +263,7 @@
     | _ =>
         (case Term.strip_comb (Thm.term_of ct) of
           (Const (c as (_, T)), ts) =>
-            if SMT_Builtin.is_builtin ctxt c
+            if SMT_Builtin.is_partially_builtin ctxt c
             then eta_args_conv norm_conv
               (length (Term.binder_types T) - length ts)
             else args_conv o norm_conv
@@ -520,6 +540,7 @@
       else SOME (i, f ctxt' thm)
   in
     irules
+    |> map (apsnd instantiate_elim)
     |> trivial_distinct ctxt
     |> rewrite_bool_cases ctxt
     |> normalize_numerals ctxt