binding replaces bstring
authorhaftmann
Mon, 09 Mar 2009 09:37:33 +0100
changeset 30379 1ae7b86638ad
parent 30378 e0247e990702
child 30380 50eec112ca1c
binding replaces bstring
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))