# HG changeset patch
# User paulson
# Date 959357237 -7200
# Node ID 8673a4d954e8e92ec3a063a77f74e93be9a38561
# Parent  718907f55f62ce7f67f40f888651cd7f3dde8e39
a more robust proof

diff -r 718907f55f62 -r 8673a4d954e8 src/HOL/UNITY/UNITY.ML
--- a/src/HOL/UNITY/UNITY.ML	Fri May 26 18:06:58 2000 +0200
+++ b/src/HOL/UNITY/UNITY.ML	Fri May 26 18:07:17 2000 +0200
@@ -55,8 +55,9 @@
 qed "surjective_mk_program";
 
 Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
-by (stac (surjective_mk_program RS sym) 1);
-by (stac (surjective_mk_program RS sym) 1 THEN Force_tac 1);
+by (res_inst_tac [("t", "F")] (surjective_mk_program RS subst) 1);
+by (res_inst_tac [("t", "G")] (surjective_mk_program RS subst) 1);
+by (Asm_simp_tac 1);
 qed "program_equalityI";
 
 val [major,minor] =