changeset 1100 | 2fb07e01c57b |
parent 1097 | 551eacf071d7 |
child 1126 | dd6ce36a0616 |
--- a/Quot/quotient_info.ML Tue Feb 09 15:36:23 2010 +0100 +++ b/Quot/quotient_info.ML Tue Feb 09 15:43:39 2010 +0100 @@ -110,7 +110,7 @@ val relname = Sign.intern_const thy relstr fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ()) - val _ = List.app sanity_check [mapname, relname] + val _ = List.app sanity_check [mapname, relname] in maps_attribute_aux tyname {mapfun = mapname, relmap = relname} end