# HG changeset patch
# User wenzelm
# Date 1363265542 -3600
# Node ID f25ee4fb437d851c3fd7a5ecd6eaa5f48bd02375
# Parent  0098bfe3be53f59abe5fe8b2059d125b43f6839c
made SML/NJ happy;

diff -r 0098bfe3be53 -r f25ee4fb437d src/HOL/Tools/Lifting/lifting_info.ML
--- 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;