changeset 58928 | 23d0ffd48006 |
parent 58919 | 82a71046dce8 |
child 59058 | a78612c67ec0 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Nov 07 16:22:25 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Nov 07 16:36:55 2014 +0100 @@ -123,7 +123,7 @@ fun thms_of_name ctxt name = let val get = maps (Proof_Context.get_fact ctxt o fst) - val keywords = Keyword.get_keywords () + val keywords = Thy_Header.get_keywords' ctxt in Source.of_string name |> Symbol.source