| changeset 59582 | 0fbed69ff081 |
| parent 59058 | a78612c67ec0 |
| child 59660 | 49e498cedd02 |
--- a/src/Pure/Isar/rule_cases.ML Tue Mar 03 19:08:04 2015 +0100 +++ b/src/Pure/Isar/rule_cases.ML Wed Mar 04 19:53:18 2015 +0100 @@ -195,7 +195,7 @@ fun (tac1 THEN_ALL_NEW_CASES tac2) i st = st |> tac1 i |> Seq.maps (fn (cases, st') => - CASES cases (Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st)) st'); + CASES cases (Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)) st');