src/HOLCF/Tools/Domain/domain_extender.ML

--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 14:33:34 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 14:35:09 2010 -0800
@@ -127,10 +127,10 @@
     (comp_dnam : string)
     (eqs''' : ((string * string option) list * binding * mixfix *
                (binding * (bool * binding option * 'a) list * mixfix) list) list)
-    (thy''' : theory) =
+    (thy : theory) =
   let
-    fun readS (SOME s) = Syntax.read_sort_global thy''' s
-      | readS NONE = Sign.defaultS thy''';
+    fun readS (SOME s) = Syntax.read_sort_global thy s
+      | readS NONE = Sign.defaultS thy;
     fun readTFree (a, s) = TFree (a, readS s);
 
     val dtnvs = map (fn (vs,dname:binding,mx,_) => 
@@ -138,19 +138,19 @@
     val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
     fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
     fun thy_arity (dname,tvars,mx) =
-        (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS);
-    val thy'' =
-      thy'''
+        (Sign.full_name thy dname, map (snd o dest_TFree) tvars, pcpoS);
+    val thy =
+      thy
       |> Sign.add_types (map thy_type dtnvs)
       |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
     val cons'' =
-      map (map (upd_second (map (upd_third (prep_typ thy''))))) cons''';
+      map (map (upd_second (map (upd_third (prep_typ thy))))) cons''';
     val dtnvs' =
-      map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
+      map (fn (dname,vs,mx) => (Sign.full_name thy dname,vs)) dtnvs;
     val eqs' : ((string * typ list) *
         (binding * (bool * binding option * typ) list * mixfix) list) list =
-      check_and_sort_domain false dtnvs' cons'' thy'';
-    val thy' = thy'' |> Domain_Syntax.add_syntax false eqs';
+      check_and_sort_domain false dtnvs' cons'' thy;
+    val thy = thy |> Domain_Syntax.add_syntax false eqs';
     val dts  = map (Type o fst) eqs';
     val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
     fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
@@ -164,7 +164,7 @@
         ) : cons;
     val eqs : eq list =
         map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
-    val thy = thy' |> Domain_Axioms.add_axioms false eqs' eqs;
+    val thy = thy |> Domain_Axioms.add_axioms false eqs' eqs;
     val ((rewss, take_rews), theorems_thy) =
         thy
           |> fold_map (fn (eq, (x,cs)) =>
@@ -185,10 +185,10 @@
     (comp_dnam : string)
     (eqs''' : ((string * string option) list * binding * mixfix *
                (binding * (bool * binding option * 'a) list * mixfix) list) list)
-    (thy''' : theory) =
+    (thy : theory) =
   let
-    fun readS (SOME s) = Syntax.read_sort_global thy''' s
-      | readS NONE = Sign.defaultS thy''';
+    fun readS (SOME s) = Syntax.read_sort_global thy s
+      | readS NONE = Sign.defaultS thy;
     fun readTFree (a, s) = TFree (a, readS s);
 
     val dtnvs = map (fn (vs,dname:binding,mx,_) => 
@@ -196,10 +196,10 @@
     val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
     fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
     fun thy_arity (dname,tvars,mx) =
-      (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, @{sort rep});
+      (Sign.full_name thy dname, map (snd o dest_TFree) tvars, @{sort rep});
 
     (* this theory is used just for parsing and error checking *)
-    val tmp_thy = thy'''
+    val tmp_thy = thy
       |> Theory.copy
       |> Sign.add_types (map thy_type dtnvs)
       |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
@@ -207,7 +207,7 @@
     val cons'' : (binding * (bool * binding option * typ) list * mixfix) list list =
       map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons''';
     val dtnvs' : (string * typ list) list =
-      map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs;
+      map (fn (dname,vs,mx) => (Sign.full_name thy dname,vs)) dtnvs;
     val eqs' : ((string * typ list) *
         (binding * (bool * binding option * typ) list * mixfix) list) list =
       check_and_sort_domain true dtnvs' cons'' tmp_thy;
@@ -217,13 +217,13 @@
         if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
     fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
     
-    val (iso_infos, thy'') = thy''' |>
+    val (iso_infos, thy) = thy |>
       Domain_Isomorphism.domain_isomorphism
         (map (fn ((vs, dname, mx, _), eq) =>
                  (map fst vs, dname, mx, mk_eq_typ eq, NONE))
              (eqs''' ~~ eqs'))
 
-    val thy' = thy'' |> Domain_Syntax.add_syntax true eqs';
+    val thy = thy |> Domain_Syntax.add_syntax true eqs';
     val dts  = map (Type o fst) eqs';
     val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
     fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
@@ -237,7 +237,7 @@
         ) : cons;
     val eqs : eq list =
         map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
-    val thy = thy' |> Domain_Axioms.add_axioms true eqs' eqs;
+    val thy = thy |> Domain_Axioms.add_axioms true eqs' eqs;
     val ((rewss, take_rews), theorems_thy) =
         thy
           |> fold_map (fn (eq, (x,cs)) =>