# HG changeset patch
# User paulson
# Date 962182322 -7200
# Node ID 77658111e1228f4d25425bda27d2088b47906388
# Parent  5b6b65c90eeb04636bb4435b7d6ccd5dddef0b20
fixed some abuses of addDs and addEs

diff -r 5b6b65c90eeb -r 77658111e122 src/HOL/TLA/TLA.ML
--- a/src/HOL/TLA/TLA.ML	Wed Jun 28 10:50:27 2000 +0200
+++ b/src/HOL/TLA/TLA.ML	Wed Jun 28 10:52:02 2000 +0200
@@ -946,7 +946,7 @@
             Force_tac 1,
             etac STL4E 1,
             rtac DmdImpl 1,
-            force_tac (temp_css addSEs2 [prem RS wf_irrefl]) 1
+            force_tac (temp_css addIs2 [prem RS wf_irrefl]) 1
            ]);
 
 (* In particular, for natural numbers, if n decreases infinitely often
@@ -972,8 +972,8 @@
 
 qed_goal "aallI" TLA.thy 
   "[| basevars vs; (!!x. basevars (x,vs) ==> sigma |= F x) |] ==> sigma |= (AALL x. F x)"
-  (fn prems => [auto_tac (temp_css addsimps2 [aall_def] addSEs2 [eexE] 
-                                   addSIs2 prems addSDs2 prems)]);
+  (fn [prem1,prem2] => [auto_tac (temp_css addsimps2 [aall_def] addSEs2 [eexE] 
+                                   addSIs2 [prem1] addSDs2 [prem2])]);
 
 qed_goalw "aallE" TLA.thy [aall_def] "|- (AALL x. F x) --> F x"
    (K [Clarsimp_tac 1, etac swap 1,