src/HOL/Tools/record.ML
changeset 35430 df2862dc23a8
parent 35410 1ea89d2a1bd4
child 35614 d7afa8700622
     1.1 --- a/src/HOL/Tools/record.ML	Wed Mar 03 00:28:22 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Wed Mar 03 00:32:14 2010 +0100
     1.3 @@ -697,10 +697,8 @@
     1.4    let
     1.5      fun get_sort env xi =
     1.6        the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname));
     1.7 -    val map_sort = Sign.intern_sort thy;
     1.8    in
     1.9 -    Syntax.typ_of_term (get_sort (Syntax.term_sorts map_sort t)) map_sort t
    1.10 -    |> Sign.intern_tycons thy
    1.11 +    Syntax.typ_of_term (get_sort (Syntax.term_sorts t)) t
    1.12    end;
    1.13  
    1.14  
    1.15 @@ -752,8 +750,8 @@
    1.16  
    1.17                      val more' = mk_ext rest;
    1.18                    in
    1.19 -                    (* FIXME authentic syntax *)
    1.20 -                    list_comb (Syntax.const (suffix ext_typeN ext), alphas' @ [more'])
    1.21 +                    list_comb
    1.22 +                      (Syntax.const (Syntax.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
    1.23                    end
    1.24                | NONE => err ("no fields defined for " ^ ext))
    1.25            | NONE => err (name ^ " is no proper field"))
    1.26 @@ -857,7 +855,7 @@
    1.27      val T = decode_type thy t;
    1.28      val varifyT = varifyT (Term.maxidx_of_typ T);
    1.29  
    1.30 -    val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts) o Sign.extern_typ thy;
    1.31 +    val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts);
    1.32  
    1.33      fun strip_fields T =
    1.34        (case T of
    1.35 @@ -922,8 +920,7 @@
    1.36  
    1.37      fun mk_type_abbr subst name alphas =
    1.38        let val abbrT = Type (name, map (fn a => varifyT (TFree (a, Sign.defaultS thy))) alphas) in
    1.39 -        Syntax.term_of_typ (! Syntax.show_sorts)
    1.40 -          (Sign.extern_typ thy (Envir.norm_type subst abbrT))
    1.41 +        Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT)
    1.42        end;
    1.43  
    1.44      fun match rT T = Sign.typ_match thy (varifyT rT, T) Vartab.empty;
    1.45 @@ -946,14 +943,14 @@
    1.46  
    1.47  fun record_ext_type_tr' name =
    1.48    let
    1.49 -    val ext_type_name = suffix ext_typeN name;
    1.50 +    val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
    1.51      fun tr' ctxt ts =
    1.52        record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
    1.53    in (ext_type_name, tr') end;
    1.54  
    1.55  fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
    1.56    let
    1.57 -    val ext_type_name = suffix ext_typeN name;
    1.58 +    val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
    1.59      fun tr' ctxt ts =
    1.60        record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt
    1.61          (list_comb (Syntax.const ext_type_name, ts));
    1.62 @@ -1949,8 +1946,7 @@
    1.63          val (args', more) = chop_last args;
    1.64          fun mk_ext' ((name, T), args) more = mk_ext (name, T) (args @ [more]);
    1.65          fun build Ts =
    1.66 -          fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args'))
    1.67 -            more;
    1.68 +          fold_rev mk_ext' (drop n ((extension_names ~~ Ts) ~~ chunks parent_chunks args')) more;
    1.69        in
    1.70          if more = HOLogic.unit
    1.71          then build (map_range recT (parent_len + 1))
    1.72 @@ -1960,27 +1956,25 @@
    1.73      val r_rec0 = mk_rec all_vars_more 0;
    1.74      val r_rec_unit0 = mk_rec (all_vars @ [HOLogic.unit]) 0;
    1.75  
    1.76 -    fun r n = Free (rN, rec_schemeT n)
    1.77 +    fun r n = Free (rN, rec_schemeT n);
    1.78      val r0 = r 0;
    1.79 -    fun r_unit n = Free (rN, recT n)
    1.80 +    fun r_unit n = Free (rN, recT n);
    1.81      val r_unit0 = r_unit 0;
    1.82 -    val w = Free (wN, rec_schemeT 0)
    1.83 +    val w = Free (wN, rec_schemeT 0);
    1.84  
    1.85  
    1.86      (* print translations *)
    1.87  
    1.88 -    val external_names = Name_Space.external_names (Sign.naming_of ext_thy);
    1.89 -
    1.90      val record_ext_type_abbr_tr's =
    1.91        let
    1.92 -        val trnames = external_names (hd extension_names);
    1.93 +        val trname = hd extension_names;
    1.94          val last_ext = unsuffix ext_typeN (fst extension);
    1.95 -      in map (record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0) trnames end;
    1.96 +      in [record_ext_type_abbr_tr' name alphas zeta last_ext rec_schemeT0 trname] end;
    1.97  
    1.98      val record_ext_type_tr's =
    1.99        let
   1.100          (*avoid conflict with record_type_abbr_tr's*)
   1.101 -        val trnames = if parent_len > 0 then external_names extension_name else [];
   1.102 +        val trnames = if parent_len > 0 then [extension_name] else [];
   1.103        in map record_ext_type_tr' trnames end;
   1.104  
   1.105      val advanced_print_translation =