src/Pure/Isar/local_defs.ML
changeset 21684 e8c135b166b3
parent 21591 5e0f2340caa7
child 21687 f689f729afab
     1.1 --- a/src/Pure/Isar/local_defs.ML	Wed Dec 06 21:19:00 2006 +0100
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Wed Dec 06 21:19:01 2006 +0100
     1.3 @@ -10,6 +10,7 @@
     1.4    val cert_def: Proof.context -> term -> (string * typ) * term
     1.5    val abs_def: term -> (string * typ) * term
     1.6    val mk_def: Proof.context -> (string * term) list -> term list
     1.7 +  val expand: cterm list -> thm -> thm
     1.8    val def_export: Assumption.export
     1.9    val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
    1.10      (term * (bstring * thm)) list * Proof.context
    1.11 @@ -68,11 +69,17 @@
    1.12    -----------
    1.13        B a
    1.14  *)
    1.15 -fun def_export _ defs thm =
    1.16 -  thm
    1.17 -  |> Drule.implies_intr_list defs
    1.18 -  |> Drule.generalize ([], map (head_of_def o Thm.term_of) defs)
    1.19 -  |> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
    1.20 +fun expand defs =
    1.21 +  Drule.implies_intr_list defs
    1.22 +  #> Drule.generalize ([], map (head_of_def o Thm.term_of) defs)
    1.23 +  #> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
    1.24 +
    1.25 +fun expand_term [] = I
    1.26 +  | expand_term defs = Pattern.rewrite_term
    1.27 +      (Theory.merge_list (map Thm.theory_of_cterm defs))
    1.28 +      (map (Logic.dest_equals o Thm.prop_of o Assumption.assume) defs) [];
    1.29 +
    1.30 +fun def_export _ defs = (expand defs, expand_term defs);
    1.31  
    1.32  
    1.33  (* add defs *)
    1.34 @@ -94,7 +101,7 @@
    1.35    end;
    1.36  
    1.37  
    1.38 -(* export -- result based on educated guessing *)
    1.39 +(* specific export -- result based on educated guessing *)
    1.40  
    1.41  fun export inner outer th =
    1.42    let