# HG changeset patch
# User wenzelm
# Date 1152178009 -7200
# Node ID 815393c02db94e5eb933bc867a327c848d611f6d
# Parent  9e7d3d06c643bd2eeb4b8f96e061f7debf827199
def_export: Drule.generalize;

diff -r 9e7d3d06c643 -r 815393c02db9 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Thu Jul 06 11:26:46 2006 +0200
+++ b/src/Pure/Isar/local_defs.ML	Thu Jul 06 11:26:49 2006 +0200
@@ -56,9 +56,9 @@
 
 (* export defs *)
 
-fun head_of_def cprop =
-  Term.head_of (#1 (Logic.dest_equals (Term.strip_all_body (Thm.term_of cprop))))
-  |> Thm.cterm_of (Thm.theory_of_cterm cprop);
+val head_of_def =
+  #1 o Term.dest_Free o Term.head_of o #1 o Logic.dest_equals o Term.strip_all_body o Thm.term_of;
+
 
 (*
   [x, x == t]
@@ -70,8 +70,7 @@
 fun def_export _ cprops thm =
   thm
   |> Drule.implies_intr_list cprops
-  |> Drule.forall_intr_list (map head_of_def cprops)
-  |> Drule.forall_elim_vars 0
+  |> Drule.generalize ([], map head_of_def cprops)
   |> RANGE (replicate (length cprops) (Tactic.rtac Drule.reflexive_thm)) 1;