adm_tac extended

--- a/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Sep 09 11:14:20 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Sep 09 11:15:32 1997 +0200
@@ -296,7 +296,7 @@
 \         trans_of(restrict ioa acts) = trans_of(ioa) & \
 \         reachable (restrict ioa acts) s = reachable ioa s & \
 \         act (restrict A acts) = act A";
-by (simp_tac (!simpset addsimps [cancel_restrict_a,cancel_restrict_b,acts_restrict]) 1);
+  by (simp_tac (!simpset addsimps [cancel_restrict_a,cancel_restrict_b,acts_restrict]) 1);
 qed"cancel_restrict";
 
 (* ---------------------------------------------------------------------------------- *)

--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Sep 09 11:14:20 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Sep 09 11:15:32 1997 +0200
@@ -7,9 +7,6 @@
 
 *)
 
-(* re-add extended adm_tactic, as it has been lost during theory merge *) 
-simpset := !simpset addSolver(fn thms =>
-            (adm_tac (cut_facts_tac thms THEN' cont_tacRs)));
 
 Addsimps [andalso_and,andalso_or];