Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
changeset 60638 16d80e5ef2dc
parent 59582 0fbed69ff081
child 65458 cf504b7a7aa7 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jul 03 14:32:55 2015 +0200
@@ -220,7 +220,7 @@
     t
 
 fun theory_const_prop_of fudge th =
-  theory_constify fudge (Context.theory_name (Thm.theory_of_thm th)) (Thm.prop_of th)
+  theory_constify fudge (Thm.theory_name_of_thm th) (Thm.prop_of th)
 
 fun pair_consts_fact thy fudge fact =
   (case fact |> snd |> theory_const_prop_of fudge |> pconsts_in_fact thy of
isabelle