src/Pure/Proof/extraction.ML
changeset 27691 ce171cbd4b93
parent 27330 1af2598b5f7d
child 27865 27a8ad9612a3
     1.1 --- a/src/Pure/Proof/extraction.ML	Tue Jul 29 08:15:39 2008 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Tue Jul 29 08:15:40 2008 +0200
     1.3 @@ -729,7 +729,7 @@
     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_i false [((extr_name s vs ^ "_def",
     1.8 +               |> PureThy.add_defs false [((extr_name s vs ^ "_def",
     1.9                      Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]
    1.10             in
    1.11               thy'