# HG changeset patch
# User wenzelm
# Date 1365589483 -7200
# Node ID 7fbc4fc400d8b6a4aa2b4f44d32a39736cd3705f
# Parent  5e1108291c7fabe1b342416e893f8000414158d8
proper proof context;
removed historic comments;

diff -r 5e1108291c7f -r 7fbc4fc400d8 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Apr 10 11:51:56 2013 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Apr 10 12:24:43 2013 +0200
@@ -5,8 +5,6 @@
 a tactic to analyse instances of the fresh_fun.
 *)
 
-(* First some functions that should be in the library *)  (* FIXME really?? *)
-
 (* FIXME proper ML structure *)
 
 (* FIXME res_inst_tac mostly obsolete, cf. Subgoal.FOCUS *)
@@ -46,8 +44,6 @@
   Global_Theory.get_thm thy name handle ERROR _ =>
     error ("The atom type "^atom_name^" is not defined.");
 
-(* End of function waiting to be in the library :o) *)
-
 (* The theorems needed that are known at compile time. *)
 val at_exists_fresh' = @{thm "at_exists_fresh'"};
 val fresh_fun_app'   = @{thm "fresh_fun_app'"};
@@ -127,14 +123,13 @@
   curry (curry (FIRST' (map uncurry (map uncurry (map subst_inner_asm_tac_aux
             (1 upto Thm.nprems_of th)))))) ctxt th;
 
-fun fresh_fun_tac no_asm i thm =
+fun fresh_fun_tac ctxt no_asm i thm =
   (* Find the variable we instantiate *)
   let
     val thy = theory_of_thm thm;
-    val ctxt = Proof_Context.init_global thy;
-    val ss = global_simpset_of thy;
     val abs_fresh = Global_Theory.get_thms thy "abs_fresh";
     val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app";
+    val ss = simpset_of ctxt;
     val ss' = ss addsimps fresh_prod::abs_fresh;
     val ss'' = ss' addsimps fresh_perm_app;
     val x = hd (tl (Misc_Legacy.term_vars (prop_of exI)));
@@ -194,5 +189,5 @@
     (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
 
 fun setup_fresh_fun_simp x =
-  (Scan.lift options_syntax >> (fn b => K (SIMPLE_METHOD' (fresh_fun_tac b)))) x;
+  (Scan.lift options_syntax >> (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b))) x;