src/Pure/Isar/rule_cases.ML
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;