Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Tools/inductive_package.ML
changeset 12243 a2c0aaf94460
parent 12227 c654c2c03f1d
child 12720 f8a134b9a57f 
--- a/src/ZF/Tools/inductive_package.ML	Mon Nov 19 20:47:39 2001 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Mon Nov 19 20:47:57 2001 +0100
@@ -152,7 +152,7 @@
 
 
   val dummy = conditional verbose (fn () =>
-    writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ big_rec_name));
+    writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ quote big_rec_name));
 
   (*Forbid the inductive definition structure from clashing with a theory
     name.  This restriction may become obsolete as ML is de-emphasized.*)
isabelle