--- a/src/HOL/Tools/SMT2/z3_new_replay.ML Thu Jun 12 01:00:49 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay.ML Thu Jun 12 01:00:49 2014 +0200
@@ -71,8 +71,8 @@
in Inttab.update (id, (fixes, replay_thm ctxt assumed nthms step)) proofs end
local
- val remove_trigger = mk_meta_eq @{thm SMT2.trigger_def}
- val remove_fun_app = mk_meta_eq @{thm SMT2.fun_app_def}
+ val remove_trigger = mk_meta_eq @{thm trigger_def}
+ val remove_fun_app = mk_meta_eq @{thm fun_app_def}
fun rewrite_conv _ [] = Conv.all_conv
| rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs)
@@ -97,7 +97,7 @@
assms
|> map (apsnd (rewrite ctxt eqs'))
|> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
- |> Z3_New_Replay_Util.thm_net_of snd
+ |> Z3_New_Replay_Util.thm_net_of snd
fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
@@ -159,7 +159,7 @@
fun discharge_assms_tac rules =
REPEAT (HEADGOAL (resolve_tac (intro_def_rules @ rules) ORELSE' SOLVED' discharge_sk_tac))
-
+
fun discharge_assms ctxt rules thm =
(if Thm.nprems_of thm = 0 then
thm