src/HOL/Tools/SMT/smt_normalize.ML
changeset 60642 48dd1cefb4ae
parent 59632 5980e75a204e
child 61033 fd7fe96ca7b9
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Fri Jul 03 16:19:45 2015 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Sun Jul 05 15:02:30 2015 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  
     1.5    fun inst f ct thm =
     1.6      let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
     1.7 -    in Thm.instantiate ([], [(cv, ct)]) thm end
     1.8 +    in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end
     1.9  in
    1.10  
    1.11  fun instantiate_elim thm =
    1.12 @@ -199,8 +199,10 @@
    1.13  
    1.14    fun insert_trigger_conv [] ct = Conv.all_conv ct
    1.15      | insert_trigger_conv ctss ct =
    1.16 -        let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct
    1.17 -        in Thm.instantiate ([], [cp, (ctr, mk_trigger ctss)]) trigger_eq end
    1.18 +        let
    1.19 +          val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct
    1.20 +          val inst = map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)]
    1.21 +        in Thm.instantiate ([], inst) trigger_eq end
    1.22  
    1.23    fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct =
    1.24      let