# HG changeset patch
# User wenzelm
# Date 1238257309 -3600
# Node ID cabf9ff3a129c7e0c57a38d4f6b3dfb737ea1af7
# Parent  ac7570d80c3d29edc36a79859d8c97fb1198e8f0
define_prefs: removed redundant Drule.gen_all, which is already part of the norm_hhf stage of Assumption.assume;

diff -r ac7570d80c3d -r cabf9ff3a129 src/Pure/Isar/expression.ML
--- 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';