--- 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