diff -r 203e5552496b -r 332fab43628f src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Aug 29 22:31:36 2000 +0200
+++ b/src/HOL/simpdata.ML	Wed Aug 30 10:21:19 2000 +0200
@@ -480,6 +480,37 @@
 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 attrib_setup =
+ [Attrib.add_attributes
+  [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
+
+end;
 
 (*** integration of simplifier with classical reasoner ***)