# HG changeset patch
# User wenzelm
# Date 1164811498 -3600
# Node ID 5e0f2340caa7cca2113016f844af75b2a3800404
# Parent  ef7278f553eb9801f7ff187233f7f0282fb2bb8c
added export;
removed find_def, expand_defs;

diff -r ef7278f553eb -r 5e0f2340caa7 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Wed Nov 29 15:44:57 2006 +0100
+++ b/src/Pure/Isar/local_defs.ML	Wed Nov 29 15:44:58 2006 +0100
@@ -13,8 +13,7 @@
   val def_export: Assumption.export
   val add_defs: ((string * mixfix) * ((bstring * attribute list) * term)) list -> Proof.context ->
     (term * (bstring * thm)) list * Proof.context
-  val find_def: Proof.context -> string -> thm option
-  val expand_defs: Proof.context -> Proof.context -> thm -> thm list * thm
+  val export: Proof.context -> Proof.context -> thm -> thm list * thm
   val print_rules: Proof.context -> unit
   val defn_add: attribute
   val defn_del: attribute
@@ -95,21 +94,17 @@
   end;
 
 
-(* find/expand defs -- based on educated guessing *)
+(* export -- result based on educated guessing *)
 
-fun find_def ctxt x =
-  Assumption.prems_of ctxt |> find_first (fn th =>
-    (case try (head_of_def o Thm.prop_of) th of
-      SOME y => x = y
-    | NONE => false));
-
-fun expand_defs inner outer th =
+fun export inner outer th =
   let
     val th' = Assumption.export false inner outer th;
-    val xs = map #1 (Drule.fold_terms Term.add_frees th []);
-    val ys = map #1 (Drule.fold_terms Term.add_frees th' []);
-    val defs = map_filter (find_def inner) (subtract (op =) ys xs);
-  in (defs, th') end;
+    val still_fixed = map #1 (Drule.fold_terms Term.add_frees th' []);
+    val defs = Assumption.prems_of inner |> filter_out (fn prem =>
+      (case try (head_of_def o Thm.prop_of) prem of
+        SOME x => member (op =) still_fixed x
+      | NONE => true));
+  in (map Drule.abs_def defs, th') end;