src/HOLCF/IOA/meta_theory/Automata.ML
changeset 4473 803d1e302af1
parent 4423 a129b817b58a
child 4477 b3e5857d8d99
--- a/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Dec 23 11:47:13 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Dec 23 11:49:46 1997 +0100
@@ -205,7 +205,7 @@
 by (eres_inst_tac [("x","a")] allE 1);
 by (eres_inst_tac [("x","a")] allE 1);
 by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
-by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
+by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1);
 by (dtac inpAAactB_is_inpBoroutB 1);
 back();
 by (assume_tac 1);