# HG changeset patch
# User wenzelm
# Date 1392036451 -3600
# Node ID e61e023c9fafaa92b16a2dcbe87b50a12e492b9b
# Parent  d79c057c68f07912a404c6686cf0ea9fa0840be3
removed rotten code;

diff -r d79c057c68f0 -r e61e023c9faf src/HOL/Statespace/DistinctTreeProver.thy
--- a/src/HOL/Statespace/DistinctTreeProver.thy	Mon Feb 10 13:04:08 2014 +0100
+++ b/src/HOL/Statespace/DistinctTreeProver.thy	Mon Feb 10 13:47:31 2014 +0100
@@ -632,82 +632,4 @@
 
 ML_file "distinct_tree_prover.ML"
 
-(* Uncomment for profiling or debugging *)
-(*
-ML {*
-(*
-val nums = (0 upto 10000);
-val nums' = (200 upto 3000);
-*)
-val nums = (0 upto 10000);
-val nums' = (0 upto 3000);
-val const_decls = map (fn i => ("const" ^ string_of_int i, Type ("nat", []), NoSyn)) nums
-
-val consts = sort Term_Ord.fast_term_ord 
-              (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)
-val consts' = sort Term_Ord.fast_term_ord 
-              (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums')
-
-val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts
-
-
-val t' = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts'
-
-
-val dist = 
-     HOLogic.Trueprop$
-       (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t)
-
-val dist' = 
-     HOLogic.Trueprop$
-       (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t')
-
-val da = Unsynchronized.ref refl;
-
-*}
-
-setup {*
-Theory.add_consts_i const_decls
-#> (fn thy  => let val ([thm],thy') = Global_Theory.add_axioms [(("dist_axiom",dist),[])] thy
-               in (da := thm; thy') end)
-*}
-
-
-ML {* 
- val ct' = cterm_of @{theory} t';
-*}
-
-ML {*
- timeit (fn () => (DistinctTreeProver.subtractProver (term_of ct') ct' (!da);())) 
-*}
-
-(* 590 s *)
-
-ML {*
-
-
-val p1 = 
- the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const1",Type ("nat",[]))) t)
-val p2 =
- the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const10000",Type ("nat",[]))) t)
-*}
-
-
-ML {* timeit (fn () => DistinctTreeProver.distinctTreeProver (!da )
-       p1
-       p2)*}
-
-
-ML {* timeit (fn () => (DistinctTreeProver.deleteProver (!da) p1;())) *}
-
-
-
-
-ML {*
-val cdist' = cterm_of @{theory} dist';
-DistinctTreeProver.distinct_implProver (!da) cdist';
-*}
-
-*)
-
 end