1.1 --- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Nov 08 14:09:07 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon Nov 08 14:36:17 2010 -0800
     1.3 @@ -426,8 +426,8 @@
     1.4      (* this theory is used just for parsing *)
     1.5      val tmp_thy = thy |>
     1.6        Theory.copy |>
     1.7 -      Sign.add_types (map (fn (tvs, tname, mx, _, morphs) =>
     1.8 -        (tname, length tvs, mx)) doms_raw);
     1.9 +      Sign.add_types (map (fn (tvs, tbind, mx, _, morphs) =>
    1.10 +        (tbind, length tvs, mx)) doms_raw);
    1.11  
    1.12      fun prep_dom thy (vs, t, mx, typ_raw, morphs) sorts =
    1.13        let val (typ, sorts') = prep_typ thy typ_raw sorts
    1.14 @@ -437,9 +437,12 @@
    1.15           sorts : (string * sort) list) =
    1.16        fold_map (prep_dom tmp_thy) doms_raw [];
    1.17  
    1.18 +    (* lookup function for sorts of type variables *)
    1.19 +    fun the_sort v = the (AList.lookup (op =) sorts v);
    1.20 +
    1.21      (* domain equations *)
    1.22      fun mk_dom_eqn (vs, tbind, mx, rhs, morphs) =
    1.23 -      let fun arg v = TFree (v, the (AList.lookup (op =) sorts v));
    1.24 +      let fun arg v = TFree (v, the_sort v);
    1.25        in (Type (Sign.full_name tmp_thy tbind, map arg vs), rhs) end;
    1.26      val dom_eqns = map mk_dom_eqn doms;
    1.27  
    1.28 @@ -460,14 +463,14 @@
    1.29  
    1.30      (* determine deflation combinator arguments *)
    1.31      fun defl_flags (vs, tbind, mx, rhs, morphs) =
    1.32 -      let fun argT v = TFree (v, the (AList.lookup (op =) sorts v));
    1.33 +      let fun argT v = TFree (v, the_sort v);
    1.34        in map (is_bifinite thy o argT) vs end;
    1.35      val defl_flagss = map defl_flags doms;
    1.36  
    1.37      (* declare deflation combinator constants *)
    1.38      fun declare_defl_const (vs, tbind, mx, rhs, morphs) thy =
    1.39        let
    1.40 -        fun argT v = TFree (v, the (AList.lookup (op =) sorts v));
    1.41 +        fun argT v = TFree (v, the_sort v);
    1.42          val Ts = map argT vs;
    1.43          val flags = map (is_bifinite thy) Ts;
    1.44          val defl_type = mk_defl_type flags Ts;
    1.45 @@ -497,7 +500,7 @@
    1.46      (* define types using deflation combinators *)
    1.47      fun make_repdef ((vs, tbind, mx, _, _), defl_const) thy =
    1.48        let
    1.49 -        fun tfree a = TFree (a, the (AList.lookup (op =) sorts a));
    1.50 +        fun tfree a = TFree (a, the_sort a);
    1.51          val Ts = map tfree vs;
    1.52          val type_args = map Logic.mk_type (filter_out (is_bifinite thy) Ts);
    1.53          val defl_args = map mk_DEFL (filter (is_bifinite thy) Ts);