--- a/src/HOL/ex/predicate_compile.ML Mon Mar 09 09:34:39 2009 +0100
+++ b/src/HOL/ex/predicate_compile.ML Mon Mar 09 09:37:33 2009 +0100
@@ -677,7 +677,7 @@
val lhs = list_comb (Const (mode_id, funT), xparams @ xins)
val def = Logic.mk_equals (lhs, predterm)
val ([defthm], thy') = thy |>
- Sign.add_consts_i [(NameSpace.base_name mode_id, funT, NoSyn)] |>
+ Sign.add_consts_i [(Binding.name (NameSpace.base_name mode_id), funT, NoSyn)] |>
PureThy.add_defs false [((Binding.name (NameSpace.base_name mode_id ^ "_def"), def), [])]
in thy' |> map_names (PredModetab.update_new ((name, mode), mode_id))
|> map_function_defs (Symtab.update_new (mode_id, defthm))