# HG changeset patch
# User haftmann
# Date 1274885097 -7200
# Node ID 6ba1b0ef0cc48f0ad06be24f3514287255f3f493
# Parent  e0bd5934a2fb4f9c151b47773ce40ac70594dd47
dropped legacy theorem bindings

diff -r e0bd5934a2fb -r 6ba1b0ef0cc4 src/HOLCF/IOA/Modelcheck/MuIOA.thy
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Wed May 26 16:31:44 2010 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Wed May 26 16:44:57 2010 +0200
@@ -276,13 +276,13 @@
 OldGoals.by (REPEAT (dtac eq_reflection 1));
 (* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
 OldGoals.by (full_simp_tac ((global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs)
-                              delsimps [not_iff,split_part])
+                              delsimps [not_iff, @{thm split_part}])
                               addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
                                         rename_simps @ ioa_simps @ asig_simps)) 1);
 OldGoals.by (full_simp_tac
-  (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1);
+  (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff, @{thm split_part}]) 1);
 OldGoals.by (REPEAT (if_full_simp_tac
-  (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
+  (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff, @{thm split_part}]) 1));
 OldGoals.by (call_mucke_tac 1);
 (* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
 OldGoals.by (atac 1);
diff -r e0bd5934a2fb -r 6ba1b0ef0cc4 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed May 26 16:31:44 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed May 26 16:44:57 2010 +0200
@@ -1101,7 +1101,7 @@
   THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (simpset_of ctxt) i)));
 
 fun pair_tac ctxt s =
-  res_inst_tac ctxt [(("p", 0), s)] PairE
+  res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
   THEN' hyp_subst_tac THEN' asm_full_simp_tac (simpset_of ctxt);
 
 (* induction on a sequence of pairs with pairsplitting and simplification *)