changeset 3842 | b55686a7b22c |
parent 3792 | 1ecbaca6560a |
child 3945 | ae9c61d69888 |
--- a/src/HOL/datatype.ML Fri Oct 10 18:37:49 1997 +0200 +++ b/src/HOL/datatype.ML Fri Oct 10 19:02:28 1997 +0200 @@ -341,7 +341,7 @@ 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;