# HG changeset patch
# User wenzelm
# Date 1004904006 -3600
# Node ID d38b5388e695f5acc62c887b1085ec6f52314759
# Parent  e151e66da2d6a429b3503a3261367eb4f3043f5e
added get_thms_with_closure;
fix_frees: only new ones;

diff -r e151e66da2d6 -r d38b5388e695 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Nov 04 20:59:01 2001 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Nov 04 21:00:06 2001 +0100
@@ -71,6 +71,7 @@
   val get_thm_closure: context -> string -> thm
   val get_thms: context -> string -> thm list
   val get_thms_closure: context -> string -> thm list
+  val get_thms_with_closure: (string -> thm list) -> context -> string -> thm list
   val put_thm: string * thm -> context -> context
   val put_thms: string * thm list -> context -> context
   val put_thmss: (string * thm list) list -> context -> context
@@ -788,6 +789,7 @@
 val get_thm_closure = retrieve_thms PureThy.get_thms_closure PureThy.single_thm;
 val get_thms = retrieve_thms PureThy.get_thms (K I);
 val get_thms_closure = retrieve_thms PureThy.get_thms_closure (K I);
+fun get_thms_with_closure closure = retrieve_thms (K closure) (K I);
 
 
 (* put_thm(s) *)
@@ -943,7 +945,7 @@
     val xs = flat (map fst varss);
   in
     (case Library.duplicates xs of [] => () | dups => err_dups ctxt dups);
-    ctxt' |> map_vars (add ctxt xs)
+    ctxt' |> map_vars (add ctxt (rev xs))
   end;
 
 in
@@ -954,9 +956,12 @@
 
 end;
 
-fun fix_frees ts =
-  let val frees = foldl (foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs)) ([], ts)
-  in fix_direct (map (fn (x, T) => ([x], Some T)) frees) end;
+fun fix_frees ts ctxt =
+  let
+    val frees = foldl (foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs)) ([], ts);
+    val fixed = fixed_names ctxt;
+    fun new (x, T) = if x mem_string fixed then None else Some ([x], Some T);
+  in fix_direct (mapfilter new frees) ctxt end;
 
 
 (*Note: improper use may result in variable capture / dynamic scoping!*)