def_export: Drule.generalize;
authorwenzelm
Thu Jul 06 11:26:49 2006 +0200 (2006-07-06 ago)
changeset 20021815393c02db9
parent 20020 9e7d3d06c643
child 20022 b07a138b4e7d
def_export: Drule.generalize;
src/Pure/Isar/local_defs.ML
     1.1 --- a/src/Pure/Isar/local_defs.ML	Thu Jul 06 11:26:46 2006 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Jul 06 11:26:49 2006 +0200
     1.3 @@ -56,9 +56,9 @@
     1.4  
     1.5  (* export defs *)
     1.6  
     1.7 -fun head_of_def cprop =
     1.8 -  Term.head_of (#1 (Logic.dest_equals (Term.strip_all_body (Thm.term_of cprop))))
     1.9 -  |> Thm.cterm_of (Thm.theory_of_cterm cprop);
    1.10 +val head_of_def =
    1.11 +  #1 o Term.dest_Free o Term.head_of o #1 o Logic.dest_equals o Term.strip_all_body o Thm.term_of;
    1.12 +
    1.13  
    1.14  (*
    1.15    [x, x == t]
    1.16 @@ -70,8 +70,7 @@
    1.17  fun def_export _ cprops thm =
    1.18    thm
    1.19    |> Drule.implies_intr_list cprops
    1.20 -  |> Drule.forall_intr_list (map head_of_def cprops)
    1.21 -  |> Drule.forall_elim_vars 0
    1.22 +  |> Drule.generalize ([], map head_of_def cprops)
    1.23    |> RANGE (replicate (length cprops) (Tactic.rtac Drule.reflexive_thm)) 1;
    1.24  
    1.25