tuned;
authorwenzelm
Mon Jun 03 13:49:35 2019 +0200 (6 weeks ago)
changeset 70305959e167798f0
parent 70304 1514efa1e57a
child 70306 61621dc439d4
tuned;
src/Pure/Isar/local_defs.ML
     1.1 --- a/src/Pure/Isar/local_defs.ML	Mon Jun 03 13:28:01 2019 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Mon Jun 03 13:49:35 2019 +0200
     1.3 @@ -249,14 +249,14 @@
     1.4        |> (snd o Logic.dest_equals o Thm.prop_of)
     1.5        |> conditional ? Logic.strip_imp_concl
     1.6        |> (abs_def o #2 o cert_def ctxt get_pos);
     1.7 -    fun prove ctxt' def =
     1.8 -      Goal.prove ctxt'
     1.9 -        ((not (Variable.is_body ctxt') ? Variable.add_free_names ctxt' prop) []) [] prop
    1.10 -        (fn {context = ctxt'', ...} =>
    1.11 +    fun prove def_ctxt def =
    1.12 +      Goal.prove def_ctxt
    1.13 +        ((not (Variable.is_body def_ctxt) ? Variable.add_free_names def_ctxt prop) []) [] prop
    1.14 +        (fn {context = goal_ctxt, ...} =>
    1.15            ALLGOALS
    1.16 -            (CONVERSION (meta_rewrite_conv ctxt'') THEN'
    1.17 -              rewrite_goal_tac ctxt'' [def] THEN'
    1.18 -              resolve_tac ctxt'' [Drule.reflexive_thm]))
    1.19 +            (CONVERSION (meta_rewrite_conv goal_ctxt) THEN'
    1.20 +              rewrite_goal_tac goal_ctxt [def] THEN'
    1.21 +              resolve_tac goal_ctxt [Drule.reflexive_thm]))
    1.22        handle ERROR msg => cat_error msg "Failed to prove definitional specification";
    1.23    in (((c, T), rhs), prove) end;
    1.24