--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Tue Aug 17 14:01:39 1999 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Tue Aug 17 15:59:32 1999 +0200
@@ -49,8 +49,8 @@
\ @@ (x>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`t))";
by (rtac trans 1);
by (stac oraclebuild_unfold 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
-by (simp_tac (simpset() addsimps [Cons_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
+by (simp_tac (simpset() addsimps [Consq_def]) 1);
qed"oraclebuild_cons";