changeset 58950 | d07464875dd4 |
parent 58014 | 47ecbef7274b |
child 59058 | a78612c67ec0 |
--- a/src/Pure/Isar/rule_cases.ML Sat Nov 08 17:39:01 2014 +0100 +++ b/src/Pure/Isar/rule_cases.ML Sat Nov 08 21:31:51 2014 +0100 @@ -221,7 +221,7 @@ th |> unfold_prems ctxt n defs |> unfold_prems_concls ctxt defs - |> Drule.multi_resolve (take m facts) + |> Drule.multi_resolve (SOME ctxt) (take m facts) |> Seq.map (pair (xx, (n - m, drop m facts))) end;