changeset 40722 | 441260986b63 |
parent 40315 | 11846d9800de |
child 40840 | 2f97215e79bf |
--- a/src/HOL/Tools/record.ML Fri Nov 26 22:04:33 2010 +0100 +++ b/src/HOL/Tools/record.ML Fri Nov 26 22:29:41 2010 +0100 @@ -917,7 +917,7 @@ val fields' = extern f :: map Long_Name.base_name fs; val (args', more) = split_last args; in (fields' ~~ args') @ strip_fields more end - handle Library.UnequalLengths => [("", t)]) + handle ListPair.UnequalLengths => [("", t)]) | NONE => [("", t)]) | NONE => [("", t)]) | _ => [("", t)]);