--- a/src/HOL/MicroJava/J/Conform.thy Wed May 26 16:28:55 2010 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy Wed May 26 16:31:44 2010 +0200
@@ -328,8 +328,8 @@
apply auto
apply(rule hconfI)
apply(drule conforms_heapD)
-apply(tactic {* auto_tac (HOL_cs addEs [thm "oconf_hext"]
- addDs [thm "hconfD"], @{simpset} delsimps [split_paired_All]) *})
+apply(tactic {* auto_tac (HOL_cs addEs [@{thm oconf_hext}]
+ addDs [@{thm hconfD}], @{simpset} delsimps [@{thm split_paired_All}]) *})
done
lemma conforms_upd_local:
--- a/src/HOL/Modelcheck/MuckeSyn.thy Wed May 26 16:28:55 2010 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy Wed May 26 16:31:44 2010 +0200
@@ -228,7 +228,7 @@
EVERY [
REPEAT (etac thin_rl i),
cut_facts_tac (mk_lam_defs defs) i,
- full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i,
+ full_simp_tac (Mucke_ss delsimps [not_iff, @{thm split_part}]) i,
move_mus i, call_mucke_tac i,atac i,
REPEAT (rtac refl i)] state);
*}