src/Pure/Isar/local_defs.ML
changeset 20021 815393c02db9
parent 19897 fe661eb3b0e7
child 20049 f48c4a3a34bc
--- 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;