src/Pure/Proof/extraction.ML
changeset 29579 cb520b766e00
parent 29270 0eade173f77e
child 29635 31d14e9fa0da
     1.1 --- a/src/Pure/Proof/extraction.ML	Wed Jan 21 16:47:03 2009 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Wed Jan 21 16:47:04 2009 +0100
     1.3 @@ -733,11 +733,11 @@
     1.4               val (def_thms, thy') = if t = nullt then ([], thy) else
     1.5                 thy
     1.6                 |> Sign.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)]
     1.7 -               |> PureThy.add_defs false [((extr_name s vs ^ "_def",
     1.8 +               |> PureThy.add_defs false [((Binding.name (extr_name s vs ^ "_def"),
     1.9                      Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
    1.10             in
    1.11               thy'
    1.12 -             |> PureThy.store_thm (corr_name s vs,
    1.13 +             |> PureThy.store_thm (Binding.name (corr_name s vs),
    1.14                    Thm.varifyT (funpow (length (OldTerm.term_vars corr_prop))
    1.15                      (Thm.forall_elim_var 0) (forall_intr_frees
    1.16                        (ProofChecker.thm_of_proof thy'