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