src/Pure/Isar/local_defs.ML

       |> Thm.cterm_of ctxt
       |> meta_rewrite_conv ctxt
       |> (snd o Logic.dest_equals o Thm.prop_of)
       |> conditional ? Logic.strip_imp_concl
       |> (abs_def o #2 o cert_def ctxt get_pos);
-    fun prove ctxt' def =
-      Goal.prove ctxt'
-        ((not (Variable.is_body ctxt') ? Variable.add_free_names ctxt' prop) []) [] prop
-        (fn {context = ctxt'', ...} =>
+    fun prove def_ctxt def =
+      Goal.prove def_ctxt
+        ((not (Variable.is_body def_ctxt) ? Variable.add_free_names def_ctxt prop) []) [] prop
+        (fn {context = goal_ctxt, ...} =>
           ALLGOALS
-            (CONVERSION (meta_rewrite_conv ctxt'') THEN'
-              rewrite_goal_tac ctxt'' [def] THEN'
-              resolve_tac ctxt'' [Drule.reflexive_thm]))
+            (CONVERSION (meta_rewrite_conv goal_ctxt) THEN'
+              rewrite_goal_tac goal_ctxt [def] THEN'
+              resolve_tac goal_ctxt [Drule.reflexive_thm]))
       handle ERROR msg => cat_error msg "Failed to prove definitional specification";
   in (((c, T), rhs), prove) end;
 
 end;