src/HOL/record.ML
changeset 4574 b922012cc142
parent 4564 dc45cf21dbd2
     1.1 --- a/src/HOL/record.ML	Wed Jan 14 10:32:24 1998 +0100
     1.2 +++ b/src/HOL/record.ML	Wed Jan 14 11:10:19 1998 +0100
     1.3 @@ -69,7 +69,7 @@
     1.4        val paras_args = map (op ~~) (record_parass thy info ~~ record_argss thy info);
     1.5        val raw_substs = map typ_subst_TVars paras_args;
     1.6        fun make_substs [] = []
     1.7 -        | make_substs (x::xs) = (foldr1 (op o) (x::xs)) :: make_substs xs; 
     1.8 +        | make_substs (x::xs) = (foldr1 (op o) (rev (x::xs))) :: make_substs xs; 
     1.9        val free_TFree = map (map (map_type_tfree (fn (str, s) => TVar((str, 0), s))));
    1.10        val raw_record_field_types = map (map snd o #fields) (record_infos thy (Some info))
    1.11      in 
    1.12 @@ -349,14 +349,14 @@
    1.13              |> Theory.add_defs_i 
    1.14                    ((make_defs make_schemeT makeT base_frees z thy) @ 
    1.15                     (sel_defs recT r all_fields current_fullfields) @
    1.16 -                   (update_defs recT r all_fields current_fullfields thy))
    1.17 +                   (update_defs recT r all_fields current_fullfields thy)) 
    1.18        in 
    1.19          thy |> PureThy.store_thmss 
    1.20                   [("record_simps", 
    1.21                     sel_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @  
    1.22                     sel_make_thms recT_unitT makeT base_frees all_fields full thy @
    1.23                     update_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @
    1.24 -                   update_make_thms recT_unitT makeT base_frees all_fields full thy )] 
    1.25 +                   update_make_thms recT_unitT makeT base_frees all_fields full thy )]
    1.26              |> Theory.add_path ".." 
    1.27        end
    1.28