# HG changeset patch
# User paulson
# Date 918044964 -3600
# Node ID 8a505e0694d0e19e9473ff03e3e3902d5b9cc942
# Parent  cd237a10cbf8210baa73deebaed72c2ff3be5506
standard spelling: type-checking

diff -r cd237a10cbf8 -r 8a505e0694d0 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Wed Feb 03 13:26:07 1999 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Wed Feb 03 13:29:24 1999 +0100
@@ -228,7 +228,7 @@
      rewrite_goals_tac con_defs,
      REPEAT (rtac refl 2),
      (*Typechecking; this can fail*)
-     if !Ind_Syntax.trace then print_tac "The typechecking subgoal:"
+     if !Ind_Syntax.trace then print_tac "The type-checking subgoal:"
      else all_tac,
      REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
 			ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2::