equal
deleted
inserted
replaced
205 |> the_default "Main"; |
205 |> the_default "Main"; |
206 val with_dups = is_some (args "with_dups"); |
206 val with_dups = is_some (args "with_dups"); |
207 |
207 |
208 fun do_find () = |
208 fun do_find () = |
209 let |
209 let |
210 val ctxt = ProofContext.init_global (theory thy_name); |
210 val ctxt = ProofContext.init_global (Thy_Info.get_theory thy_name); |
211 val query = get_query (); |
211 val query = get_query (); |
212 val (othmslen, thms) = apsnd rev |
212 val (othmslen, thms) = apsnd rev |
213 (Find_Theorems.find_theorems ctxt NONE (SOME limit) with_dups query); |
213 (Find_Theorems.find_theorems ctxt NONE (SOME limit) with_dups query); |
214 val thmslen = length thms; |
214 val thmslen = length thms; |
215 fun thm_row args = Xhtml.write send (html_thm ctxt args); |
215 fun thm_row args = Xhtml.write send (html_thm ctxt args); |