--- a/src/HOL/TLA/TLA.thy Thu May 12 22:35:15 2011 +0200
+++ b/src/HOL/TLA/TLA.thy Thu May 12 22:37:31 2011 +0200
@@ -138,10 +138,6 @@
declare tempI [intro!]
declare tempD [dest]
-ML {*
-val temp_css = (@{claset}, @{simpset})
-val temp_cs = op addss temp_css
-*}
(* Modify the functions that add rules to simpsets, classical sets,
and clasimpsets in order to accept "lifted" theorems
@@ -427,12 +423,6 @@
lemmas temp_simps [temp_rewrite, simp] = BoxConst DmdConst
-(* Make these rewrites active by default *)
-ML {*
-val temp_css = temp_css addsimps2 @{thms temp_simps}
-val temp_cs = op addss temp_css
-*}
-
(* ------------------------ Further rewrites ----------------------------------------- *)
section "Further rewrites"