# HG changeset patch
# User wenzelm
# Date 1152356088 -7200
# Node ID 080ca1f8afd78fcd1789872df34ae36ad3209bc2
# Parent  25935807eb082f597c06d1f668fc7a01b38e0f88
removed dead code;

diff -r 25935807eb08 -r 080ca1f8afd7 src/Pure/Tools/codegen_simtype.ML
--- a/src/Pure/Tools/codegen_simtype.ML	Sat Jul 08 12:54:47 2006 +0200
+++ b/src/Pure/Tools/codegen_simtype.ML	Sat Jul 08 12:54:48 2006 +0200
@@ -56,19 +56,10 @@
   |> Proof.theorem_i PureThy.internalK NONE after_qed NONE ("", [])
        (map (fn t => (("", []), [(t, [])])) props);
 
-fun tactic_proof tac after_qed props thy =
-  let
-    val thms = Goal.prove_multi thy [] [] props (K tac);
-  in
-    thy
-    |> after_qed thms
-  end;
-
 in
 
 val simtype = gen_e_simtype setup_proof;
 val simtype_i = gen_i_simtype setup_proof;
-val prove_simtype = gen_i_simtype o tactic_proof;
 
 end; (*local*)