src/HOL/Modelcheck/MuckeSyn.thy

--- a/src/HOL/Modelcheck/MuckeSyn.thy	Wed Sep 17 21:27:08 2008 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Wed Sep 17 21:27:14 2008 +0200
@@ -236,11 +236,6 @@
         full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i,
         move_mus i, call_mucke_tac i,atac i,
         REPEAT (rtac refl i)] state);
-
-(*check if user has mucke installed*)
-fun mucke_enabled () = getenv "MUCKE_HOME" <> "";
-fun if_mucke_enabled f x = if mucke_enabled () then f x else ();
-
 *}
 
 end