changeset 43232 | 23f352990944 |
parent 43050 | 24662b614fd4 |
child 43314 | 724e612ba248 |
1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Apr 16 15:47:52 2011 +0200 1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Apr 16 16:15:37 2011 +0200 1.3 @@ -411,7 +411,7 @@ 1.4 fun thms_of_name ctxt name = 1.5 let 1.6 val lex = Keyword.get_lexicons 1.7 - val get = maps (ProofContext.get_fact ctxt o fst) 1.8 + val get = maps (Proof_Context.get_fact ctxt o fst) 1.9 in 1.10 Source.of_string name 1.11 |> Symbol.source