define_prefs: removed redundant Drule.gen_all, which is already part of the norm_hhf stage of Assumption.assume;

--- a/src/Pure/Isar/expression.ML	Sat Mar 28 17:21:11 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Mar 28 17:21:49 2009 +0100
@@ -654,13 +654,13 @@
 
 fun define_preds pname parms (((exts, exts'), (ints, ints')), defs) thy =
   let
-    val defs' = map (cterm_of thy #> Assumption.assume #> Drule.gen_all #> Drule.abs_def) defs;
+    val defs' = map (cterm_of thy #> Assumption.assume #> Drule.abs_def) defs;
 
     val (a_pred, a_intro, a_axioms, thy'') =
       if null exts then (NONE, NONE, [], thy)
       else
         let
-          val aname = if null ints then pname else Binding.suffix_name ("_" ^ axiomsN) pname
+          val aname = if null ints then pname else Binding.suffix_name ("_" ^ axiomsN) pname;
           val ((statement, intro, axioms), thy') =
             thy
             |> def_pred aname parms defs' exts exts';