# HG changeset patch
# User narasche
# Date 884772619 -3600
# Node ID b922012cc142e966b2903bbf711c2343f2b8893f
# Parent  fe504f608835eecab5fbad406244d313e4785274
error with instantiantion of sub-records removed

diff -r fe504f608835 -r b922012cc142 src/HOL/record.ML
--- a/src/HOL/record.ML	Wed Jan 14 10:32:24 1998 +0100
+++ b/src/HOL/record.ML	Wed Jan 14 11:10:19 1998 +0100
@@ -69,7 +69,7 @@
       val paras_args = map (op ~~) (record_parass thy info ~~ record_argss thy info);
       val raw_substs = map typ_subst_TVars paras_args;
       fun make_substs [] = []
-        | make_substs (x::xs) = (foldr1 (op o) (x::xs)) :: make_substs xs; 
+        | make_substs (x::xs) = (foldr1 (op o) (rev (x::xs))) :: make_substs xs; 
       val free_TFree = map (map (map_type_tfree (fn (str, s) => TVar((str, 0), s))));
       val raw_record_field_types = map (map snd o #fields) (record_infos thy (Some info))
     in 
@@ -349,14 +349,14 @@
             |> Theory.add_defs_i 
                   ((make_defs make_schemeT makeT base_frees z thy) @ 
                    (sel_defs recT r all_fields current_fullfields) @
-                   (update_defs recT r all_fields current_fullfields thy))
+                   (update_defs recT r all_fields current_fullfields thy)) 
       in 
         thy |> PureThy.store_thmss 
                  [("record_simps", 
                    sel_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @  
                    sel_make_thms recT_unitT makeT base_frees all_fields full thy @
                    update_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @
-                   update_make_thms recT_unitT makeT base_frees all_fields full thy )] 
+                   update_make_thms recT_unitT makeT base_frees all_fields full thy )]
             |> Theory.add_path ".." 
       end