# HG changeset patch
# User wenzelm
# Date 1165436341 -3600
# Node ID e8c135b166b308fe7589f0734c82b088e7dca941
# Parent  b90fa6c8e062d3c0e92c6eebcac328ee7caa372c
added expand;
export: added explicit term operation;

diff -r b90fa6c8e062 -r e8c135b166b3 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Wed Dec 06 21:19:00 2006 +0100
+++ b/src/Pure/Isar/local_defs.ML	Wed Dec 06 21:19:01 2006 +0100
@@ -10,6 +10,7 @@
   val cert_def: Proof.context -> term -> (string * typ) * term
   val abs_def: term -> (string * typ) * term
   val mk_def: Proof.context -> (string * term) list -> term list
+  val expand: cterm list -> thm -> thm
   val def_export: Assumption.export
   val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
     (term * (bstring * thm)) list * Proof.context
@@ -68,11 +69,17 @@
   -----------
       B a
 *)
-fun def_export _ defs thm =
-  thm
-  |> Drule.implies_intr_list defs
-  |> Drule.generalize ([], map (head_of_def o Thm.term_of) defs)
-  |> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
+fun expand defs =
+  Drule.implies_intr_list defs
+  #> Drule.generalize ([], map (head_of_def o Thm.term_of) defs)
+  #> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
+
+fun expand_term [] = I
+  | expand_term defs = Pattern.rewrite_term
+      (Theory.merge_list (map Thm.theory_of_cterm defs))
+      (map (Logic.dest_equals o Thm.prop_of o Assumption.assume) defs) [];
+
+fun def_export _ defs = (expand defs, expand_term defs);
 
 
 (* add defs *)
@@ -94,7 +101,7 @@
   end;
 
 
-(* export -- result based on educated guessing *)
+(* specific export -- result based on educated guessing *)
 
 fun export inner outer th =
   let