# HG changeset patch
# User haftmann
# Date 1158673444 -7200
# Node ID 86cb35b93f01901acb2828a7d36a0146ae0946f3
# Parent  926a76a84e9731a0da6bb6cea1f24cc9540480ba
removed diagnostic messages

diff -r 926a76a84e97 -r 86cb35b93f01 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Tue Sep 19 15:31:32 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Tue Sep 19 15:44:04 2006 +0200
@@ -554,9 +554,9 @@
   val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
 in fun get_eq_datatype thy dtco =
   let
-    val _ = writeln "01";
+(*     val _ = writeln "01";  *)
     val SOME (vs, cs) = DatatypePackage.get_datatype_spec (Context.check_thy thy) dtco;
-    val _ = writeln "02";
+(*     val _ = writeln "02";  *)
     fun mk_triv_inject co =
       let
         val ct' = Thm.cterm_of (Context.check_thy thy)
@@ -567,26 +567,26 @@
           (K o SOME) (Thm.cterm_of (Context.check_thy thy) (Var (v, Thm.typ_of cty')), Thm.ctyp_of (Context.check_thy thy) ty) | _ => I)
           refl NONE;
       in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
-    val _ = writeln "03";
+(*     val _ = writeln "03";  *)
     val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
-    val _ = writeln "04";
+(*     val _ = writeln "04";  *)
     val inject2 = (#inject o DatatypePackage.the_datatype (Context.check_thy thy)) dtco;
-    val _ = writeln "05";
+(*     val _ = writeln "05";  *)
     val ctxt = Context.init_proof (Context.check_thy thy);
-    val _ = writeln "06";
+(*     val _ = writeln "06";  *)
     val simpset = Simplifier.context ctxt
       (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
-    val _ = writeln "07";
+(*     val _ = writeln "07";  *)
     val cos = map (fn (co, tys) =>
         (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
     val tac = ALLGOALS (simp_tac simpset)
       THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
-    val _ = writeln "08";
+(*     val _ = writeln "08";  *)
     val distinct =
       mk_distinct cos
       |> map (fn t => Goal.prove_global (Context.check_thy thy) [] [] t (K tac))
       |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
-    val _ = writeln "09";
+(*     val _ = writeln "09";  *)
   in inject1 @ inject2 @ distinct end;
 
 fun get_eq_typecopy thy tyco =
@@ -606,13 +606,13 @@
 in
   fun get_eq thy tyco =
     get_eq_thms (Context.check_thy thy) tyco
-    |> tap (fn _ => writeln "10")
+(*     |> tap (fn _ => writeln "10")  *)
     |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) (Context.check_thy thy))
-    |> tap (fn _ => writeln "11")
+(*     |> tap (fn _ => writeln "11")  *)
     |> constrain_op_eq (Context.check_thy thy)
-    |> tap (fn _ => writeln "12")
+(*     |> tap (fn _ => writeln "12")  *)
     |> map (Tactic.rewrite_rule [eq_def_sym])
-    |> tap (fn _ => writeln "13")
+(*     |> tap (fn _ => writeln "13")  *)
 end;
 
 end;
@@ -622,7 +622,7 @@
     val thy_ref = Theory.self_ref thy;
     val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
     val c = CodegenConsts.norm thy ("OperationalEquality.eq", [ty]);
-    val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> tap (fn _ => writeln "14x") |> rev |> tap (fn _ => writeln "15x"));
+    val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
   in
     CodegenData.add_funcl
       (c, CodegenData.lazy get_thms) thy
diff -r 926a76a84e97 -r 86cb35b93f01 src/Pure/Tools/codegen_data.ML
--- a/src/Pure/Tools/codegen_data.ML	Tue Sep 19 15:31:32 2006 +0200
+++ b/src/Pure/Tools/codegen_data.ML	Tue Sep 19 15:44:04 2006 +0200
@@ -180,9 +180,9 @@
 
 fun add_drop_redundant thm thms =
   let
-    val _ = writeln "add_drop 01";
+(*     val _ = writeln "add_drop 01";  *)
     val thy = Context.check_thy (Thm.theory_of_thm thm);
-    val _ = writeln "add_drop 02";
+(*     val _ = writeln "add_drop 02";  *)
     val pattern = (fst o Logic.dest_equals o Drule.plain_prop_of) thm;
     fun matches thm' = if (curry (Pattern.matches thy) pattern o
       fst o Logic.dest_equals o Drule.plain_prop_of) thm'