| changeset 33957 | e9afca2118d4 |
| parent 33955 | fff6f11b1f09 |
| child 34982 | 7b8c366e34a2 |
--- a/src/Pure/Isar/proof_context.ML Tue Nov 24 17:28:44 2009 +0100 +++ b/src/Pure/Isar/proof_context.ML Wed Nov 25 09:13:46 2009 +0100 @@ -1340,7 +1340,7 @@ val suppressed = len - ! prems_limit; val prt_prems = if null prems then [] else [Pretty.big_list "prems:" ((if suppressed <= 0 then [] else [Pretty.str "..."]) @ - map (Display.pretty_thm ctxt) ((uncurry drop) (suppressed, prems)))]; + map (Display.pretty_thm ctxt) (drop suppressed prems))]; in prt_structs @ prt_fixes @ prt_prems end;