diff -r a94029edb01f -r bcd0ee8d71aa Datatype.ML
--- a/Datatype.ML	Fri Jul 08 12:01:55 1994 +0200
+++ b/Datatype.ML	Fri Jul 08 17:22:58 1994 +0200
@@ -6,7 +6,8 @@
 
 
 (*choice between Ci_neg1 and Ci_neg2 axioms depends on number of constructors*)
-val dtK = 5;
+local val dtK = 5
+in
 
 local open ThyParse in
 val datatype_decls =
@@ -25,7 +26,7 @@
       val typ =
          ident                  >> (cat "dtId" o quote)
         ||
-         type_var_list -- ident >> (fn (ts, id) => "Comp (" ^ mk_list ts ^
+         type_var_list -- ident >> (fn (ts, id) => "dtComp (" ^ mk_list ts ^
   				  ", " ^ quote id ^ ")")
         ||
          tvar;
@@ -90,12 +91,12 @@
 (*used for constructor parameters*)
 datatype dt_type = dtVar of string |
                    dtId  of string |
-                   Comp of dt_type list * string |
-                   Rek of dt_type list * string;
+                   dtComp of dt_type list * string |
+                   dtRek of dt_type list * string;
 
-exception Impossible;
-
-local open Syntax.Mixfix in
+local open Syntax.Mixfix
+      exception Impossible
+in
 fun add_datatype (typevars, tname, cons_list') thy = 
   let fun cat s1 s2 = s1 ^ " " ^ s2;
 
@@ -119,23 +120,23 @@
                   | analyse ((dtId s) :: typlist) =
                      if tname<>s then (dtId s) :: analyse typlist
                      else if null typevars then 
-                       Rek ([], tname) :: analyse typlist
+                       dtRek ([], tname) :: analyse typlist
                      else error (s ^ " used in different ways")
-                  | analyse (Comp (typl,s) :: typlist) =
-                     if tname <> s then Comp (analyse typl, s)
+                  | analyse (dtComp (typl,s) :: typlist) =
+                     if tname <> s then dtComp (analyse typl, s)
                                      :: analyse typlist
                      else if typevars = typl then
-                       Rek (typl, s) :: analyse typlist
+                       dtRek (typl, s) :: analyse typlist
                      else 
                        error (s ^ " used in different ways")
                   | analyse [] = []
-                  | analyse ((Rek _) :: _) = raise Impossible;
+                  | analyse ((dtRek _) :: _) = raise Impossible;
             in (cons, analyse typlist, syn) end;
 
       (*test if there are elements that are not recursive, i.e. if the type is
         not empty*)
       fun one_not_rek (cs : ('a * dt_type list * 'c) list) = 
-        let val contains_no_rek = forall (fn Rek _ => false | _ => true);
+        let val contains_no_rek = forall (fn dtRek _ => false | _ => true);
         in exists (contains_no_rek o #2) cs orelse
            error("Empty type not allowed!") end;
 
@@ -147,8 +148,8 @@
         pp_typlist1: parentheses, pp_typlist2: brackets*)
       fun pp_typ (dtVar s) = s
         | pp_typ (dtId s) = s
-        | pp_typ (Comp (typvars, id)) = (pp_typlist1 typvars) ^ id
-        | pp_typ (Rek (typvars, id)) = (pp_typlist1 typvars) ^ id
+        | pp_typ (dtComp (typvars, id)) = (pp_typlist1 typvars) ^ id
+        | pp_typ (dtRek (typvars, id)) = (pp_typlist1 typvars) ^ id
       and
           pp_typlist' ts = commas (map pp_typ ts)
       and
@@ -197,7 +198,7 @@
             else s
         | create_typevar _ _ = raise Impossible;
 
-      fun assumpt (Rek _ :: ts, v :: vs ,found) =
+      fun assumpt (dtRek _ :: ts, v :: vs ,found) =
             let val h = if found then ";P(" ^ v ^ ")"
                                  else "[| P(" ^ v ^ ")"
             in h ^ (assumpt (ts, vs, true)) end
@@ -212,26 +213,26 @@
                                 else (t,s,n) :: (insert typ varname xs)
         | insert typ varname [] = [(typ, varname, 1)];
 
-      fun insert_types (Rek (l,id) :: ts) tab =
-            insert_types ts (insert (Rek(l,id)) id tab)
+      fun insert_types (dtRek (l,id) :: ts) tab =
+            insert_types ts (insert (dtRek(l,id)) id tab)
         | insert_types ((dtVar s) :: ts) tab =
             insert_types ts (insert (dtVar s) (implode (tl (explode s))) tab)
         | insert_types ((dtId s) :: ts) tab =
             insert_types ts (insert (dtId s) s tab)
-        | insert_types (Comp (l,id) :: ts) tab =
-            insert_types ts (insert (Comp(l,id)) id tab)
+        | insert_types (dtComp (l,id) :: ts) tab =
+            insert_types ts (insert (dtComp(l,id)) id tab)
         | insert_types [] tab = tab;
 
-      fun update(Rek _, s, v :: vs, (Rek _) :: ts) = s :: vs
+      fun update(dtRek _, s, v :: vs, (dtRek _) :: ts) = s :: vs
         | update(t, s, v :: vs, t1 :: ts) = 
             if t=t1 then s :: vs
                     else v :: (update (t, s, vs, ts))
         | update _ = raise Impossible;
       
-      fun update_n (Rek r1, s, v :: vs, (Rek r2) :: ts, n) =
+      fun update_n (dtRek r1, s, v :: vs, (dtRek r2) :: ts, n) =
             if r1 = r2 then (s ^ string_of_int n) :: 
-                            (update_n (Rek r1, s, vs, ts, n+1))
-                       else v :: (update_n (Rek r1, s, vs, ts, n))
+                            (update_n (dtRek r1, s, vs, ts, n+1))
+                       else v :: (update_n (dtRek r1, s, vs, ts, n))
         | update_n (t, s, v :: vs, t1 :: ts, n) = 
             if t = t1 then (s ^ string_of_int n) :: 
                            (update_n (t, s, vs, ts, n+1))
@@ -384,4 +385,5 @@
      |> add_trrules xrules
      |> add_axioms rules
   end
-end;
\ No newline at end of file
+end
+end;