src/Provers/quantifier1.ML

             if qa = q then exqu ((qC,x,T)::xs) Q else NONE
         | exqu xs P = extract (null xs) xs P
   in exqu [] end;
 
 fun prove_conv tac thy tu =
-  let val ctxt = ProofContext.init_global thy;
+  let val ctxt = Proof_Context.init_global thy;
       val eq_tu = Logic.mk_equals tu;
       val ([fixed_goal], ctxt') = Variable.import_terms true [eq_tu] ctxt;
       val thm = Goal.prove ctxt' [] [] fixed_goal
             (K (rtac iff_reflection 1 THEN tac));
       val [gen_thm] = Variable.export ctxt' ctxt [thm];