src/HOL/Tools/SMT/z3_interface.ML
changeset 59586 ddf6deaadfe8
parent 58360 dee1fd1cc631
child 59621 291934bac95e
     1.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Wed Mar 04 20:50:20 2015 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Wed Mar 04 22:05:01 2015 +0100
     1.3 @@ -136,7 +136,7 @@
     1.4  val update =
     1.5    SMT_Util.mk_const_pat @{theory} @{const_name fun_upd} (Thm.dest_ctyp o SMT_Util.destT1)
     1.6  fun mk_update array index value =
     1.7 -  let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
     1.8 +  let val cTs = Thm.dest_ctyp (Thm.ctyp_of_cterm array)
     1.9    in Thm.apply (Thm.mk_binop (SMT_Util.instTs cTs update) array index) value end
    1.10  
    1.11  val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (int)})
    1.12 @@ -166,7 +166,7 @@
    1.13    | (Sym ("select", _), [ca, ck]) => SOME (Thm.apply (mk_access ca) ck)
    1.14    | (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv)
    1.15    | _ =>
    1.16 -    (case (sym, try (#T o Thm.rep_cterm o hd) cts, cts) of
    1.17 +    (case (sym, try (Thm.typ_of_cterm o hd) cts, cts) of
    1.18        (Sym ("+", _), SOME @{typ int}, _) => SOME (mk_nary add int0 cts)
    1.19      | (Sym ("-", _), SOME @{typ int}, [ct]) => SOME (mk_uminus ct)
    1.20      | (Sym ("-", _), SOME @{typ int}, [ct, cu]) => SOME (mk_sub ct cu)