avoid home-grown meta_allE;

--- a/src/HOL/Record.thy	Fri Oct 21 18:14:34 2005 +0200
+++ b/src/HOL/Record.thy	Fri Oct 21 18:14:36 2005 +0200
@@ -8,13 +8,6 @@
 uses ("Tools/record_package.ML")
 begin
 
-ML {*
-val [h1, h2] = Goal "PROP Goal (\<And>x. PROP P x) \<Longrightarrow> (PROP P x \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q";
-by (rtac h2 1);
-by (rtac (gen_all (h1 RS Drule.rev_triv_goal)) 1);
-qed "meta_allE";
-*}
-
 lemma prop_subst: "s = t \<Longrightarrow> PROP P t \<Longrightarrow> PROP P s"
   by simp