--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Nov 28 12:25:43 2012 +0100
@@ -30,19 +30,6 @@
fun string_for_label (s, num) = s ^ string_of_int num
-fun thms_of_name ctxt name =
- let
- val lex = Keyword.get_lexicons
- val get = maps (Proof_Context.get_fact ctxt o fst)
- in
- Source.of_string name
- |> Symbol.source
- |> Token.source {do_recover = SOME false} lex Position.start
- |> Token.source_proper
- |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
- |> Source.exhaust
- end
-
val inc = curry op+
fun metis_steps_top_level proof = fold (fn Prove _ => inc 1 | _ => I) proof 0
fun metis_steps_recursive proof =