1.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Fri Aug 27 17:11:29 2010 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Fri Aug 27 17:23:57 2010 +0200
     1.3 @@ -18,8 +18,6 @@
     1.4    val eqvt_force_del: attribute
     1.5    val setup: theory -> theory
     1.6    val get_eqvt_thms: Proof.context -> thm list
     1.7 -
     1.8 -  val NOMINAL_EQVT_DEBUG : bool Unsynchronized.ref
     1.9  end;
    1.10  
    1.11  structure NominalThmDecls: NOMINAL_THMDECLS =
    1.12 @@ -44,29 +42,31 @@
    1.13  (* equality-lemma can be derived. *)
    1.14  exception EQVT_FORM of string
    1.15  
    1.16 -val NOMINAL_EQVT_DEBUG = Unsynchronized.ref false
    1.17 +val (nominal_eqvt_debug, setup_nominal_eqvt_debug) =
    1.18 +  Attrib.config_bool "nominal_eqvt_debug" (K false);
    1.19  
    1.20 -fun tactic (msg, tac) =
    1.21 -  if !NOMINAL_EQVT_DEBUG
    1.22 +fun tactic ctxt (msg, tac) =
    1.23 +  if Config.get ctxt nominal_eqvt_debug
    1.24    then tac THEN' (K (print_tac ("after " ^ msg)))
    1.25    else tac
    1.26  
    1.27  fun prove_eqvt_tac ctxt orig_thm pi pi' =
    1.28 -let
    1.29 -  val mypi = Thm.cterm_of ctxt pi
    1.30 -  val T = fastype_of pi'
    1.31 -  val mypifree = Thm.cterm_of ctxt (Const (@{const_name "rev"}, T --> T) $ pi')
    1.32 -  val perm_pi_simp = PureThy.get_thms ctxt "perm_pi_simp"
    1.33 -in
    1.34 -  EVERY1 [tactic ("iffI applied", rtac @{thm iffI}),
    1.35 -          tactic ("remove pi with perm_boolE", dtac @{thm perm_boolE}),
    1.36 -          tactic ("solve with orig_thm", etac orig_thm),
    1.37 -          tactic ("applies orig_thm instantiated with rev pi",
    1.38 -                     dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)),
    1.39 -          tactic ("getting rid of the pi on the right", rtac @{thm perm_boolI}),
    1.40 -          tactic ("getting rid of all remaining perms",
    1.41 -                     full_simp_tac (HOL_basic_ss addsimps perm_pi_simp))]
    1.42 -end;
    1.43 +  let
    1.44 +    val thy = ProofContext.theory_of ctxt
    1.45 +    val mypi = Thm.cterm_of thy pi
    1.46 +    val T = fastype_of pi'
    1.47 +    val mypifree = Thm.cterm_of thy (Const (@{const_name "rev"}, T --> T) $ pi')
    1.48 +    val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"
    1.49 +  in
    1.50 +    EVERY1 [tactic ctxt ("iffI applied", rtac @{thm iffI}),
    1.51 +            tactic ctxt ("remove pi with perm_boolE", dtac @{thm perm_boolE}),
    1.52 +            tactic ctxt ("solve with orig_thm", etac orig_thm),
    1.53 +            tactic ctxt ("applies orig_thm instantiated with rev pi",
    1.54 +                       dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)),
    1.55 +            tactic ctxt ("getting rid of the pi on the right", rtac @{thm perm_boolI}),
    1.56 +            tactic ctxt ("getting rid of all remaining perms",
    1.57 +                       full_simp_tac (HOL_basic_ss addsimps perm_pi_simp))]
    1.58 +  end;
    1.59  
    1.60  fun get_derived_thm ctxt hyp concl orig_thm pi typi =
    1.61    let
    1.62 @@ -78,7 +78,7 @@
    1.63      val _ = writeln (Syntax.string_of_term ctxt' goal_term);
    1.64    in
    1.65      Goal.prove ctxt' [] [] goal_term
    1.66 -      (fn _ => prove_eqvt_tac thy orig_thm pi' pi'') |>
    1.67 +      (fn _ => prove_eqvt_tac ctxt' orig_thm pi' pi'') |>
    1.68      singleton (ProofContext.export ctxt' ctxt)
    1.69    end
    1.70  
    1.71 @@ -170,11 +170,12 @@
    1.72  val get_eqvt_thms = Context.Proof #> Data.get;
    1.73  
    1.74  val setup =
    1.75 -    Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del) 
    1.76 -     "equivariance theorem declaration" 
    1.77 - #> Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
    1.78 -     "equivariance theorem declaration (without checking the form of the lemma)" 
    1.79 - #> PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get) 
    1.80 +  setup_nominal_eqvt_debug #>
    1.81 +  Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del) 
    1.82 +   "equivariance theorem declaration" #>
    1.83 +  Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
    1.84 +    "equivariance theorem declaration (without checking the form of the lemma)" #>
    1.85 +  PureThy.add_thms_dynamic (Binding.name "eqvts", Data.get);
    1.86  
    1.87  
    1.88  end;