# HG changeset patch
# User wenzelm
# Date 1192129841 -7200
# Node ID 0e5177e2c076c6566ac75480c2d84f9311ff8d64
# Parent  952045a8dcf22125731a5a2b84b8589a6c57ff88
added export_cterm;
tuned;

diff -r 952045a8dcf2 -r 0e5177e2c076 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Thu Oct 11 21:10:40 2007 +0200
+++ b/src/Pure/Isar/local_defs.ML	Thu Oct 11 21:10:41 2007 +0200
@@ -15,6 +15,7 @@
   val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
     (term * (bstring * thm)) list * Proof.context
   val export: Proof.context -> Proof.context -> thm -> thm list * thm
+  val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm
   val trans_terms: Proof.context -> thm list -> thm
   val trans_props: Proof.context -> thm list -> thm
   val print_rules: Proof.context -> unit
@@ -100,9 +101,16 @@
   end;
 
 
-(* specific export -- result based on educated guessing (beware of closure sizes) *)
+(* specific export -- result based on educated guessing *)
 
-fun export inner outer =
+(*
+  [xs, xs == as]
+        :
+       B xs
+  --------------
+       B as
+*)
+fun export inner outer =    (*beware of closure sizes*)
   let
     val exp = Assumption.export false inner outer;
     val prems = Assumption.prems_of inner;
@@ -117,6 +125,17 @@
     in (map Drule.abs_def defs, th') end
   end;
 
+(*
+  [xs, xs == as]
+        :
+     TERM b xs
+  --------------  and  --------------
+     TERM b as          b xs == b as
+*)
+fun export_cterm inner outer ct =
+  let val (defs, ct') = export inner outer (Drule.mk_term ct) ||> Drule.dest_term
+  in (ct', MetaSimplifier.rewrite true defs ct) end;
+
 
 (* basic transitivity reasoning -- modulo beta-eta *)