src/HOL/Nominal/nominal_fresh_fun.ML
changeset 36610 bafd82950e24
parent 35667 aa59452c913c
child 39557 fe5722fce758
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -124,7 +124,7 @@
     1.4    (* Find the variable we instantiate *)
     1.5    let
     1.6      val thy = theory_of_thm thm;
     1.7 -    val ctxt = ProofContext.init thy;
     1.8 +    val ctxt = ProofContext.init_global thy;
     1.9      val ss = global_simpset_of thy;
    1.10      val abs_fresh = PureThy.get_thms thy "abs_fresh";
    1.11      val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app";