--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Tue Mar 13 17:17:52 2012 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Tue Mar 13 20:04:24 2012 +0100
@@ -87,7 +87,7 @@
val def = Logic.mk_equals (lhs, atom)
val ([definition], thy') = thy
|> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
- |> Global_Theory.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
+ |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])]
in
(lhs, ((full_constname, [definition]) :: defs, thy'))
end
@@ -249,7 +249,7 @@
val def = Logic.mk_equals (lhs, abs_arg')
val ([definition], thy') = thy
|> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
- |> Global_Theory.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
+ |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])]
in
(list_comb (Logic.varify_global const, vars),
((full_constname, [definition])::new_defs, thy'))