src/HOL/Nominal/nominal_fresh_fun.ML
changeset 51669 7fbc4fc400d8
parent 47060 e2741ec9ae36
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Apr 10 11:51:56 2013 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Apr 10 12:24:43 2013 +0200
     1.3 @@ -5,8 +5,6 @@
     1.4  a tactic to analyse instances of the fresh_fun.
     1.5  *)
     1.6  
     1.7 -(* First some functions that should be in the library *)  (* FIXME really?? *)
     1.8 -
     1.9  (* FIXME proper ML structure *)
    1.10  
    1.11  (* FIXME res_inst_tac mostly obsolete, cf. Subgoal.FOCUS *)
    1.12 @@ -46,8 +44,6 @@
    1.13    Global_Theory.get_thm thy name handle ERROR _ =>
    1.14      error ("The atom type "^atom_name^" is not defined.");
    1.15  
    1.16 -(* End of function waiting to be in the library :o) *)
    1.17 -
    1.18  (* The theorems needed that are known at compile time. *)
    1.19  val at_exists_fresh' = @{thm "at_exists_fresh'"};
    1.20  val fresh_fun_app'   = @{thm "fresh_fun_app'"};
    1.21 @@ -127,14 +123,13 @@
    1.22    curry (curry (FIRST' (map uncurry (map uncurry (map subst_inner_asm_tac_aux
    1.23              (1 upto Thm.nprems_of th)))))) ctxt th;
    1.24  
    1.25 -fun fresh_fun_tac no_asm i thm =
    1.26 +fun fresh_fun_tac ctxt no_asm i thm =
    1.27    (* Find the variable we instantiate *)
    1.28    let
    1.29      val thy = theory_of_thm thm;
    1.30 -    val ctxt = Proof_Context.init_global thy;
    1.31 -    val ss = global_simpset_of thy;
    1.32      val abs_fresh = Global_Theory.get_thms thy "abs_fresh";
    1.33      val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app";
    1.34 +    val ss = simpset_of ctxt;
    1.35      val ss' = ss addsimps fresh_prod::abs_fresh;
    1.36      val ss'' = ss' addsimps fresh_perm_app;
    1.37      val x = hd (tl (Misc_Legacy.term_vars (prop_of exI)));
    1.38 @@ -194,5 +189,5 @@
    1.39      (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
    1.40  
    1.41  fun setup_fresh_fun_simp x =
    1.42 -  (Scan.lift options_syntax >> (fn b => K (SIMPLE_METHOD' (fresh_fun_tac b)))) x;
    1.43 +  (Scan.lift options_syntax >> (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b))) x;
    1.44