changeset 44045 | 2814ff2a6e3e |
parent 43761 | e72ba84ae58f |
child 45327 | 4a027cc86f1a |
--- a/src/Pure/Isar/proof.ML Sun Jul 31 11:13:38 2011 -0700 +++ b/src/Pure/Isar/proof.ML Mon Aug 01 12:08:53 2011 +0200 @@ -391,7 +391,7 @@ fun no_goal_cases st = map (rpair NONE) (goals st); fun goal_cases st = - Rule_Cases.make_common (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st)); + Rule_Cases.make_common (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st)); fun apply_method current_context meth state = let