# HG changeset patch
# User haftmann
# Date 1274884304 -7200
# Node ID e0bd5934a2fb4f9c151b47773ce40ac70594dd47
# Parent  ee23611b6bf25220a6eaac6c4134ecf4b60b6f2b
dropped legacy theorem bindings

diff -r ee23611b6bf2 -r e0bd5934a2fb src/HOL/MicroJava/J/Conform.thy
--- 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: 
diff -r ee23611b6bf2 -r e0bd5934a2fb src/HOL/Modelcheck/MuckeSyn.thy
--- 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);
 *}