diff -r c4ff384ee28f -r 0b2ff9541727 src/HOLCF/IOA/NTP/Abschannel.ML
--- a/src/HOLCF/IOA/NTP/Abschannel.ML	Sat Sep 03 16:49:48 2005 +0200
+++ b/src/HOLCF/IOA/NTP/Abschannel.ML	Sat Sep 03 16:50:22 2005 +0200
@@ -5,12 +5,10 @@
 Derived rules.
 *)
 
-open Abschannel;
-
-val unfold_renaming = 
- [srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, 
-   ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, rename_set_def, asig_of_def, 
-   actions_def, srch_trans_def, rsch_trans_def, ch_trans_def,starts_of_def, 
+val unfold_renaming =
+ [srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def,
+   ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, rename_set_def, asig_of_def,
+   actions_def, srch_trans_def, rsch_trans_def, ch_trans_def,starts_of_def,
    trans_of_def] @ asig_projections;
 
 Goal
@@ -55,4 +53,3 @@
               wfair_of_def, sfair_of_def,rsch_wfair_def,rsch_sfair_def]) 1);
 by (simp_tac (simpset() addsimps unfold_renaming) 1);
 qed"rsch_ioa_thm";
-