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_fact.ML
changeset 55151 f331472f1027
parent 55143 04448228381d
child 55212 5832470d956e 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Jan 26 13:45:40 2014 +0100
@@ -416,7 +416,7 @@
                  |> hackish_string_of_term ctxt
   in
     ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
-      stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)] [])
+      stature), th |> Rule_Insts.read_instantiate ctxt [((p_name, 0), p_inst)] [])
   end
 
 fun type_match thy (T1, T2) =
isabelle