# HG changeset patch # User wenzelm # Date 1559562575 -7200 # Node ID 959e167798f01d3c8830c2e885a908f6055dadfe # Parent 1514efa1e57af8ba5f64aafab3a91e20c7aa95ea tuned; diff -r 1514efa1e57a -r 959e167798f0 src/Pure/Isar/local_defs.ML --- 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;