equal
deleted
inserted
replaced
133 let |
133 let |
134 val mets = get_data (KEStore_Elems.get_mets thy) |
134 val mets = get_data (KEStore_Elems.get_mets thy) |
135 (* all mets of the respective theory PLUS of all ancestor theories*) |
135 (* all mets of the respective theory PLUS of all ancestor theories*) |
136 val fun_ids = mets |> map fun_id_of |> filter is_some |> map the |
136 val fun_ids = mets |> map fun_id_of |> filter is_some |> map the |
137 in |
137 in |
138 filter (fn (str, _) => ThyC.thyID_of_derivation_name str = Context.theory_name thy) fun_ids |
138 filter (fn (str, _) => ThyC.cut_id str = Context.theory_name thy) fun_ids |
139 end |
139 end |
140 |
140 |
141 type field = string * (term * term) |
141 type field = string * (term * term) |
142 val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory})) "unknown::'a => unknow"; |
142 val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory})) "unknown::'a => unknow"; |
143 |
143 |