# HG changeset patch
# User wenzelm
# Date 968352691 -7200
# Node ID c8ff37b637a7b93a4289e63806f3f31d8a04b187
# Parent  93d2fde0306c9fb0911df5dc8186e140866b6c19
eliminated rulify setup (now in Provers/rulify.ML);

diff -r 93d2fde0306c -r c8ff37b637a7 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Sep 07 20:51:07 2000 +0200
+++ b/src/HOL/simpdata.ML	Thu Sep 07 20:51:31 2000 +0200
@@ -432,37 +432,6 @@
 val simpsetup =
   [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; thy)];
 
-(*** conversion of -->/! into ==>/!! ***)
-
-local
-  val rules = [symmetric(thm"all_eq"),symmetric(thm"imp_eq"),Drule.norm_hhf_eq]
-  val ss = HOL_basic_ss addsimps rules
-in
-
-val rulify = zero_var_indexes o strip_shyps_warning o forall_elim_vars_safe o simplify ss;
-
-fun qed_spec_mp name = ThmDatabase.ml_store_thm(name, rulify(result()));
-
-fun qed_goal_spec_mp name thy s p = 
-	bind_thm (name, rulify (prove_goal thy s p));
-
-fun qed_goalw_spec_mp name thy defs s p = 
-	bind_thm (name, rulify (prove_goalw thy defs s p));
-
-end;
-
-local
-
-fun gen_rulify x =
-  Attrib.no_args (Drule.rule_attribute (fn _ => rulify)) x;
-
-in
-
-val rulify_attrib_setup =
- [Attrib.add_attributes
-  [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
-
-end;
 
 (*** integration of simplifier with classical reasoner ***)