--- a/src/HOL/thy_syntax.ML Thu Jan 08 18:09:07 1998 +0100
+++ b/src/HOL/thy_syntax.ML Thu Jan 08 18:09:47 1998 +0100
@@ -169,7 +169,7 @@
\val split_"^tname^"_case_asm = prove_goal thy (#2(split_"^tname^"_eqns))\n\
\ (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
^ quote tname ^ ")) \""^tname^"0\" 1,\n\
- \ ALLGOALS Asm_simp_tac]);\n\
+ \ ALLGOALS (asm_simp_tac (simpset() delsimps [split_paired_Ex]))]);\n\
\val thy = thy\n";
(*
--- a/src/HOLCF/IOA/meta_theory/Automata.ML Thu Jan 08 18:09:07 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML Thu Jan 08 18:09:47 1998 +0100
@@ -8,6 +8,7 @@
(* Has been removed from HOL-simpset, who knows why? *)
Addsimps [Let_def];
+Delsimps [split_paired_Ex];
open reachable;
--- a/src/HOLCF/IOA/meta_theory/Traces.ML Thu Jan 08 18:09:07 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML Thu Jan 08 18:09:47 1998 +0100
@@ -7,6 +7,7 @@
*)
Delsimps (ex_simps @ all_simps);
+Delsimps [split_paired_Ex];
val exec_rws = [executions_def,is_exec_frag_def];