src/Tools/WWW_Find/find_theorems.ML
changeset 37863 7f113caabcf4
parent 37216 3165bc303f66
child 38980 af73cf0dc31f
equal deleted inserted replaced
37862:ec81023c6861 37863:7f113caabcf4
   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);