# HG changeset patch
# User wenzelm
# Date 1320751226 -3600
# Node ID b24ecaa46edb9830ee12279f1c4997028cba895f
# Parent  23e5af70af07d6c6a4cc77d443922a4577db3189
clarified Local_Defs.export: avoid costly still_fixed test, return all defs;

diff -r 23e5af70af07 -r b24ecaa46edb src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Tue Nov 08 12:03:51 2011 +0100
+++ b/src/Pure/Isar/local_defs.ML	Tue Nov 08 12:20:26 2011 +0100
@@ -66,7 +66,7 @@
 (* export defs *)
 
 val head_of_def =
-  #1 o Term.dest_Free o Term.head_of o #1 o Logic.dest_equals o Term.strip_all_body;
+  Term.dest_Free o Term.head_of o #1 o Logic.dest_equals o Term.strip_all_body;
 
 
 (*
@@ -78,7 +78,7 @@
 *)
 fun expand defs =
   Drule.implies_intr_list defs
-  #> Drule.generalize ([], map (head_of_def o Thm.term_of) defs)
+  #> Drule.generalize ([], map (#1 o head_of_def o Thm.term_of) defs)
   #> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
 
 val expand_term = Envir.expand_term_frees o map (abs_def o Thm.term_of);
@@ -136,15 +136,20 @@
 fun export inner outer =    (*beware of closure sizes*)
   let
     val exp = Assumption.export false inner outer;
+    val exp_term = Assumption.export_term inner outer;
     val prems = Assumption.all_prems_of inner;
   in fn th =>
     let
       val th' = exp th;
-      val still_fixed = map #1 (Thm.fold_terms Term.add_frees th' []);
-      val defs = prems |> filter_out (fn prem =>
+      val defs = prems |> filter (fn prem =>
         (case try (head_of_def o Thm.prop_of) prem of
-          SOME x => member (op =) still_fixed x
-        | NONE => true));
+          SOME x =>
+            let val t = Free x in
+              (case try exp_term t of
+                SOME u => not (t aconv u)
+              | NONE => false)
+            end
+        | NONE => false));
     in (map Drule.abs_def defs, th') end
   end;