Quot/quotient_info.ML
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