src/Pure/Proof/extraction.ML
changeset 46909 3c73a121a387
parent 46219 426ed18eba43
child 46961 5c6955f487e5
     1.1 --- a/src/Pure/Proof/extraction.ML	Tue Mar 13 17:17:52 2012 +0000
     1.2 +++ b/src/Pure/Proof/extraction.ML	Tue Mar 13 20:04:24 2012 +0100
     1.3 @@ -728,7 +728,7 @@
     1.4                         (chtype [propT] Proofterm.symmetric_axm %> rhs %> lhs %%
     1.5                           (chtype [T, propT] Proofterm.combination_axm %> f %> f %> c %> t' %%
     1.6                             (chtype [T --> propT] Proofterm.reflexive_axm %> f) %%
     1.7 -                           PAxm (cname ^ "_def", eqn,
     1.8 +                           PAxm (Thm.def_name cname, eqn,
     1.9                               SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
    1.10                      val corr_prop = Reconstruct.prop_of corr_prf';
    1.11                      val corr_prf'' =
    1.12 @@ -792,7 +792,8 @@
    1.13               val (def_thms, thy') = if t = nullt then ([], thy) else
    1.14                 thy
    1.15                 |> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
    1.16 -               |> Global_Theory.add_defs false [((Binding.qualified_name (extr_name s vs ^ "_def"),
    1.17 +               |> Global_Theory.add_defs false
    1.18 +                  [((Binding.qualified_name (Thm.def_name (extr_name s vs)),
    1.19                      Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
    1.20             in
    1.21               thy'