src/HOL/thy_syntax.ML
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\