src/Pure/Isar/local_defs.ML

     val pp = ProofContext.pp ctxt;
     val display_term = quote o Pretty.string_of_term pp;
     fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^ display_term eq);
     val ((lhs, _), eq') = eq
       |> Sign.no_vars pp
-      |> Logic.dest_def pp Term.is_Free (ProofContext.is_fixed ctxt) (K true)
+      |> Logic.dest_def pp Term.is_Free (Variable.is_fixed ctxt) (K true)
       handle TERM (msg, _) => err msg | ERROR msg => err msg;
   in (Term.dest_Free (Term.head_of lhs), eq') end;
 
 val abs_def = Logic.abs_def #> apfst Term.dest_Free;
 

     fun prove ctxt' t def =
       let
         val thy' = ProofContext.theory_of ctxt';
         val prop' = Term.subst_atomic [(Free (c, T), t)] prop;
         val frees = Term.fold_aterms (fn Free (x, _) =>
-          if ProofContext.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop' [];
+          if Variable.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop' [];
       in
         Goal.prove thy' frees [] prop' (K (ALLGOALS
           (meta_rewrite_tac ctxt' THEN'
             Tactic.rewrite_goal_tac [def] THEN'
             Tactic.resolve_tac [Drule.reflexive_thm])))