src/HOLCF/IOA/meta_theory/CompoExecs.ML
changeset 7229 6773ba0c36d5
parent 5068 fb28eaa07e01
child 10835 f4745d77e620
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Tue Aug 17 14:01:39 1999 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Tue Aug 17 15:59:32 1999 +0200
@@ -110,7 +110,7 @@
 \                andalso (stutter2 sig`xs) (snd at))"; 
 by (rtac trans 1);
 by (stac stutter2_unfold 1);
-by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def,If_and_if]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def,If_and_if]) 1);
 by (Simp_tac 1);
 qed"stutter2_cons";