diff -r 148c241d2492 -r 41eee2e7b465 src/HOLCF/IOA/meta_theory/RefMappings.thy
--- a/src/HOLCF/IOA/meta_theory/RefMappings.thy	Fri Sep 02 15:54:47 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy	Fri Sep 02 17:23:59 2005 +0200
@@ -1,45 +1,46 @@
 (*  Title:      HOLCF/IOA/meta_theory/RefMappings.thy
     ID:         $Id$
     Author:     Olaf Müller
-
-Refinement Mappings in HOLCF/IOA.
 *)
 
-RefMappings = Traces  +
+header {* Refinement Mappings in HOLCF/IOA *}
 
-default type
+theory RefMappings
+imports Traces
+begin
+
+defaultsort type
 
 consts
-
   move         ::"[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool"
   is_ref_map   ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
   is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
- 
+
 
 defs
 
-
-move_def
-  "move ioa ex s a t ==    
-    (is_exec_frag ioa (s,ex) &  Finite ex & 
-     laststate (s,ex)=t  &     
+move_def:
+  "move ioa ex s a t ==
+    (is_exec_frag ioa (s,ex) &  Finite ex &
+     laststate (s,ex)=t  &
      mk_trace ioa$ex = (if a:ext(ioa) then a>>nil else nil))"
 
-is_ref_map_def
-  "is_ref_map f C A ==                          
-   (!s:starts_of(C). f(s):starts_of(A)) &        
-   (!s t a. reachable C s &                      
-            s -a--C-> t                 
+is_ref_map_def:
+  "is_ref_map f C A ==
+   (!s:starts_of(C). f(s):starts_of(A)) &
+   (!s t a. reachable C s &
+            s -a--C-> t
             --> (? ex. move A ex (f s) a (f t)))"
- 
-is_weak_ref_map_def
-  "is_weak_ref_map f C A ==                          
-   (!s:starts_of(C). f(s):starts_of(A)) &        
-   (!s t a. reachable C s &                      
-            s -a--C-> t     
-            --> (if a:ext(C) 
+
+is_weak_ref_map_def:
+  "is_weak_ref_map f C A ==
+   (!s:starts_of(C). f(s):starts_of(A)) &
+   (!s t a. reachable C s &
+            s -a--C-> t
+            --> (if a:ext(C)
                  then (f s) -a--A-> (f t)
-                 else (f s)=(f t)))" 
+                 else (f s)=(f t)))"
 
+ML {* use_legacy_bindings (the_context ()) *}
 
 end