equal
deleted
inserted
replaced
174 end |
174 end |
175 |
175 |
176 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*) |
176 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*) |
177 fun unknown_expl dI pbt selcts = |
177 fun unknown_expl dI pbt selcts = |
178 let |
178 let |
179 val thy = ThyC.get_theory dI |
179 val thy = Know_Store.get_via_last_thy dI |
180 val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*) |
180 val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*) |
181 val its = O_Model.add_enumerate its_ |
181 val its = O_Model.add_enumerate its_ |
182 in map flattup2 its end |
182 in map flattup2 its end |
183 |
183 |
184 (* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation |
184 (* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation |