changeset 55143 | 04448228381d |
parent 54914 | 25212efcd0de |
child 55151 | f331472f1027 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Jan 25 21:52:04 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sat Jan 25 22:06:07 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 |> read_instantiate ctxt [((p_name, 0), p_inst)] []) end fun type_match thy (T1, T2) =