104 val extend = I; |
104 val extend = I; |
105 val merge = merge_ptyps; (* relevant for store_thm, store_rls *) |
105 val merge = merge_ptyps; (* relevant for store_thm, store_rls *) |
106 ); |
106 ); |
107 fun get_thes thy = Data.get thy |
107 fun get_thes thy = Data.get thy |
108 fun add_thes thes thy = let |
108 fun add_thes thes thy = let |
109 fun add_the (thydata, theID) = |
109 fun add_the (thydata, theID) = add_thydata ([], theID) thydata |
110 if can_insert theID (Data.get thy) |
|
111 then |
|
112 if exist_the theID (Data.get thy) |
|
113 then (writeln ("*** insert: preserved " ^ strs2str theID); (fn x => x)) |
|
114 else insrt theID thydata theID |
|
115 else |
|
116 let |
|
117 val th' = fill_parents (Data.get thy) theID theID (*..*** insert: not found*) |
|
118 val th' = insrt theID thydata theID th' |
|
119 in merge_ptyps' th' end; (*...TODO improve efficiency: |
|
120 val ((exist, notexist) branch) = fill_parents ([], theID) (Data.get thy) |
|
121 (* fill_parents: can_insert (hd theID), then insert the branch built from there; |
|
122 fill_parents probably could generalise to the then-branch above *) |
|
123 in insrt_branch exist branch end (*notexist is in branch*)*) |
|
124 in Data.map (fold add_the thes) thy end; |
110 in Data.map (fold add_the thes) thy end; |
125 fun insert_fillpats fis thy = |
111 fun insert_fillpats fis thy = |
126 let |
112 let |
127 fun update_elem (theID, fillpats) = |
113 fun update_elem (theID, fillpats) = |
128 let |
114 let |