src/ZF/Tools/inductive_package.ML
changeset 12243 a2c0aaf94460
parent 12227 c654c2c03f1d
child 12720 f8a134b9a57f
     1.1 --- a/src/ZF/Tools/inductive_package.ML	Mon Nov 19 20:47:39 2001 +0100
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Mon Nov 19 20:47:57 2001 +0100
     1.3 @@ -152,7 +152,7 @@
     1.4  
     1.5  
     1.6    val dummy = conditional verbose (fn () =>
     1.7 -    writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ big_rec_name));
     1.8 +    writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ quote big_rec_name));
     1.9  
    1.10    (*Forbid the inductive definition structure from clashing with a theory
    1.11      name.  This restriction may become obsolete as ML is de-emphasized.*)