changeset 58950 | d07464875dd4 |
parent 58354 | 04ac60da613e |
child 59621 | 291934bac95e |
--- a/src/HOL/Tools/TFL/casesplit.ML Sat Nov 08 17:39:01 2014 +0100 +++ b/src/HOL/Tools/TFL/casesplit.ML Sat Nov 08 21:31:51 2014 +0100 @@ -122,7 +122,7 @@ (* check if we are a member of splitths - FIXME: quicker and more flexible with discrim net. *) fun solve_by_splitth th split = - Thm.biresolution false [(false,split)] 1 th; + Thm.biresolution (SOME ctxt) false [(false,split)] 1 th; fun split th = (case find_thms_split splitths 1 th of