--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Apr 13 17:00:02 2016 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Apr 13 18:01:05 2016 +0200
@@ -536,7 +536,7 @@
let
val ref_of_str = (* FIXME proper wrapper for parser combinators *)
suffix ";" #> Token.explode (Thy_Header.get_keywords' ctxt) Position.none
- #> Parse.xthm #> fst
+ #> Parse.thm #> fst
val thms = named_thms |> maps snd
val facts = named_thms |> map (ref_of_str o fst o fst)
val fact_override = {add = facts, del = [], only = true}