src/HOL/Nominal/nominal_atoms.ML
changeset 54742 7a86358a3c0b
parent 51717 9e7d1c139569
child 56253 83b3c110f22d
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Fri Dec 13 23:53:02 2013 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Dec 14 17:28:05 2013 +0100
     1.3 @@ -829,6 +829,7 @@
     1.4         (* instantiations.                                                 *)
     1.5         val (_, thy33) =
     1.6           let
     1.7 +             val ctxt32 = Proof_Context.init_global thy32;
     1.8  
     1.9               (* takes a theorem thm and a list of theorems [t1,..,tn]            *)
    1.10               (* produces a list of theorems of the form [t1 RS thm,..,tn RS thm] *) 
    1.11 @@ -918,7 +919,7 @@
    1.12              ||>> add_thmss_string
    1.13                let
    1.14                  val thms1 = inst_pt_at [all_eqvt];
    1.15 -                val thms2 = map (fold_rule [inductive_forall_def]) thms1
    1.16 +                val thms2 = map (fold_rule ctxt32 [inductive_forall_def]) thms1
    1.17                in
    1.18                  [(("all_eqvt", thms1 @ thms2), [NominalThmDecls.eqvt_force_add])]
    1.19                end