removed diagnostic messages
authorhaftmann
Tue Sep 19 15:44:04 2006 +0200 (2006-09-19)
changeset 2060886cb35b93f01
parent 20607 926a76a84e97
child 20609 5681da8c12ef
removed diagnostic messages
src/HOL/Tools/datatype_codegen.ML
src/Pure/Tools/codegen_data.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue Sep 19 15:31:32 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue Sep 19 15:44:04 2006 +0200
     1.3 @@ -554,9 +554,9 @@
     1.4    val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
     1.5  in fun get_eq_datatype thy dtco =
     1.6    let
     1.7 -    val _ = writeln "01";
     1.8 +(*     val _ = writeln "01";  *)
     1.9      val SOME (vs, cs) = DatatypePackage.get_datatype_spec (Context.check_thy thy) dtco;
    1.10 -    val _ = writeln "02";
    1.11 +(*     val _ = writeln "02";  *)
    1.12      fun mk_triv_inject co =
    1.13        let
    1.14          val ct' = Thm.cterm_of (Context.check_thy thy)
    1.15 @@ -567,26 +567,26 @@
    1.16            (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)
    1.17            refl NONE;
    1.18        in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
    1.19 -    val _ = writeln "03";
    1.20 +(*     val _ = writeln "03";  *)
    1.21      val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
    1.22 -    val _ = writeln "04";
    1.23 +(*     val _ = writeln "04";  *)
    1.24      val inject2 = (#inject o DatatypePackage.the_datatype (Context.check_thy thy)) dtco;
    1.25 -    val _ = writeln "05";
    1.26 +(*     val _ = writeln "05";  *)
    1.27      val ctxt = Context.init_proof (Context.check_thy thy);
    1.28 -    val _ = writeln "06";
    1.29 +(*     val _ = writeln "06";  *)
    1.30      val simpset = Simplifier.context ctxt
    1.31        (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
    1.32 -    val _ = writeln "07";
    1.33 +(*     val _ = writeln "07";  *)
    1.34      val cos = map (fn (co, tys) =>
    1.35          (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
    1.36      val tac = ALLGOALS (simp_tac simpset)
    1.37        THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
    1.38 -    val _ = writeln "08";
    1.39 +(*     val _ = writeln "08";  *)
    1.40      val distinct =
    1.41        mk_distinct cos
    1.42        |> map (fn t => Goal.prove_global (Context.check_thy thy) [] [] t (K tac))
    1.43        |> (fn thms => thms @ map (fn thm => not_sym OF [thm]) thms)
    1.44 -    val _ = writeln "09";
    1.45 +(*     val _ = writeln "09";  *)
    1.46    in inject1 @ inject2 @ distinct end;
    1.47  
    1.48  fun get_eq_typecopy thy tyco =
    1.49 @@ -606,13 +606,13 @@
    1.50  in
    1.51    fun get_eq thy tyco =
    1.52      get_eq_thms (Context.check_thy thy) tyco
    1.53 -    |> tap (fn _ => writeln "10")
    1.54 +(*     |> tap (fn _ => writeln "10")  *)
    1.55      |> maps ((#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) (Context.check_thy thy))
    1.56 -    |> tap (fn _ => writeln "11")
    1.57 +(*     |> tap (fn _ => writeln "11")  *)
    1.58      |> constrain_op_eq (Context.check_thy thy)
    1.59 -    |> tap (fn _ => writeln "12")
    1.60 +(*     |> tap (fn _ => writeln "12")  *)
    1.61      |> map (Tactic.rewrite_rule [eq_def_sym])
    1.62 -    |> tap (fn _ => writeln "13")
    1.63 +(*     |> tap (fn _ => writeln "13")  *)
    1.64  end;
    1.65  
    1.66  end;
    1.67 @@ -622,7 +622,7 @@
    1.68      val thy_ref = Theory.self_ref thy;
    1.69      val ty = Type (dtco, map TFree vs) |> Logic.varifyT;
    1.70      val c = CodegenConsts.norm thy ("OperationalEquality.eq", [ty]);
    1.71 -    val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> tap (fn _ => writeln "14x") |> rev |> tap (fn _ => writeln "15x"));
    1.72 +    val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
    1.73    in
    1.74      CodegenData.add_funcl
    1.75        (c, CodegenData.lazy get_thms) thy
     2.1 --- a/src/Pure/Tools/codegen_data.ML	Tue Sep 19 15:31:32 2006 +0200
     2.2 +++ b/src/Pure/Tools/codegen_data.ML	Tue Sep 19 15:44:04 2006 +0200
     2.3 @@ -180,9 +180,9 @@
     2.4  
     2.5  fun add_drop_redundant thm thms =
     2.6    let
     2.7 -    val _ = writeln "add_drop 01";
     2.8 +(*     val _ = writeln "add_drop 01";  *)
     2.9      val thy = Context.check_thy (Thm.theory_of_thm thm);
    2.10 -    val _ = writeln "add_drop 02";
    2.11 +(*     val _ = writeln "add_drop 02";  *)
    2.12      val pattern = (fst o Logic.dest_equals o Drule.plain_prop_of) thm;
    2.13      fun matches thm' = if (curry (Pattern.matches thy) pattern o
    2.14        fst o Logic.dest_equals o Drule.plain_prop_of) thm'