--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Mar 04 19:53:18 2015 +0100
@@ -310,7 +310,7 @@
fun get_prover ctxt name params goal all_facts =
let
- val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (prop_of goal) all_facts
+ val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (Thm.prop_of goal) all_facts
in
Sledgehammer_Prover_Minimize.get_minimizing_prover ctxt Sledgehammer_Prover.Normal learn name
end