--- a/src/HOL/Tools/Lifting/lifting_info.ML Thu Mar 14 10:51:28 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Thu Mar 14 13:52:22 2013 +0100
@@ -167,7 +167,7 @@
fun print_quotients ctxt =
let
- fun prt_quot (qty_name, {quot_thm, pcrel_info}) =
+ fun prt_quot (qty_name, {quot_thm, pcrel_info}: quotients) =
Pretty.block (separate (Pretty.brk 2)
[Pretty.str "type:",
Pretty.str qty_name,
@@ -429,4 +429,4 @@
Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
(Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
-end;
\ No newline at end of file
+end;