clarified context: prefer abstract Variable.auto_fixes;
authorwenzelm
Mon Jun 03 14:26:21 2019 +0200 (6 weeks ago)
changeset 7030661621dc439d4
parent 70305 959e167798f0
child 70307 53d21039518a
clarified context: prefer abstract Variable.auto_fixes;
src/Pure/Isar/local_defs.ML
     1.1 --- a/src/Pure/Isar/local_defs.ML	Mon Jun 03 13:49:35 2019 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Mon Jun 03 14:26:21 2019 +0200
     1.3 @@ -249,15 +249,22 @@
     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 def_ctxt def =
     1.8 -      Goal.prove def_ctxt
     1.9 -        ((not (Variable.is_body def_ctxt) ? Variable.add_free_names def_ctxt prop) []) [] prop
    1.10 -        (fn {context = goal_ctxt, ...} =>
    1.11 -          ALLGOALS
    1.12 -            (CONVERSION (meta_rewrite_conv goal_ctxt) THEN'
    1.13 -              rewrite_goal_tac goal_ctxt [def] THEN'
    1.14 -              resolve_tac goal_ctxt [Drule.reflexive_thm]))
    1.15 -      handle ERROR msg => cat_error msg "Failed to prove definitional specification";
    1.16 +    fun prove def_ctxt0 def =
    1.17 +      let
    1.18 +        val def_ctxt = Variable.auto_fixes prop def_ctxt0;
    1.19 +        val def_thm =
    1.20 +          Goal.prove def_ctxt [] [] prop
    1.21 +            (fn {context = goal_ctxt, ...} =>
    1.22 +              ALLGOALS
    1.23 +                (CONVERSION (meta_rewrite_conv goal_ctxt) THEN'
    1.24 +                  rewrite_goal_tac goal_ctxt [def] THEN'
    1.25 +                  resolve_tac goal_ctxt [Drule.reflexive_thm]))
    1.26 +          handle ERROR msg => cat_error msg "Failed to prove definitional specification";
    1.27 +      in
    1.28 +        def_thm
    1.29 +        |> singleton (Variable.export def_ctxt def_ctxt0)
    1.30 +        |> Drule.zero_var_indexes
    1.31 +      end;
    1.32    in (((c, T), rhs), prove) end;
    1.33  
    1.34  end;