changeset 36960 | 01594f816e3a |
parent 36959 | f5417836dbea |
child 37507 | de91b800c34e |
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 17 15:11:25 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 17 23:54:15 2010 +0200 @@ -330,7 +330,7 @@ fun thms_of_name ctxt name = let - val lex = OuterKeyword.get_lexicons + val lex = Keyword.get_lexicons val get = maps (ProofContext.get_fact ctxt o fst) in Source.of_string name