changeset 1465 | 5d7a7e439cec |
parent 1430 | 439e1476a7f8 |
child 1475 | 7f5a4cd08209 |
--- a/src/HOL/thy_syntax.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/thy_syntax.ML Tue Jan 30 15:24:36 1996 +0100 @@ -72,7 +72,7 @@ \\t val thy\t\t= thy\n\ \\t val monos\t\t= " ^ monos ^ "\n\ \\t val con_defs\t\t= " ^ con_defs ^ ");\n\n\ - \ in\n\ + \ in\n\ \ struct\n\ \ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\ \ open Result\n\