src/HOL/datatype.ML

         | assumpt _ = raise Impossible;
 
       fun t_inducting ((_, name, types, vns, _) :: cs) =
         let
           val h = if null types then " P(" ^ name ^ ")"
-                  else " !!" ^ (space_implode " " vns) ^ "." ^
+                  else " !!" ^ (space_implode " " vns) ^ ". " ^
                     (assumpt (types, vns, false)) ^
                     "P(" ^ C_exp name vns ^ ")";
           val rest = t_inducting cs;
         in if rest = "" then h else h ^ "; " ^ rest end
         | t_inducting [] = "";