--- a/src/Pure/Isar/local_defs.ML Mon Jun 03 13:28:01 2019 +0200
+++ b/src/Pure/Isar/local_defs.ML Mon Jun 03 13:49:35 2019 +0200
@@ -249,14 +249,14 @@
|> (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;