# HG changeset patch
# User haftmann
# Date 1236587853 -3600
# Node ID 1ae7b86638ad279855ae61881a0a075f59a64459
# Parent  e0247e990702f20784cb8b6dae46b5b832d356f0
binding replaces bstring

diff -r e0247e990702 -r 1ae7b86638ad src/HOL/ex/predicate_compile.ML
--- 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))