# HG changeset patch
# User wenzelm
# Date 1266608494 -3600
# Node ID 18ae6ef02fe09f27caf78ddd32856ff94ce8a6d4
# Parent  b625eb708d9434c9de3865ebec94e752f4aae938
Thm.def_binding;

diff -r b625eb708d94 -r 18ae6ef02fe0 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Fri Feb 19 20:39:48 2010 +0100
+++ b/src/HOL/Tools/typedef.ML	Fri Feb 19 20:41:34 2010 +0100
@@ -119,8 +119,7 @@
       if def then
         theory
         |> Sign.add_consts_i [(name, setT', NoSyn)]   (* FIXME authentic syntax *)
-        |> PureThy.add_defs false
-          [((Binding.map_name Thm.def_name name, Logic.mk_equals (setC, set)), [])]
+        |> PureThy.add_defs false [((Thm.def_binding name, Logic.mk_equals (setC, set)), [])]
         |-> (fn [th] => pair (SOME th))
       else (NONE, theory);
     fun contract_def NONE th = th
diff -r b625eb708d94 -r 18ae6ef02fe0 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Feb 19 20:39:48 2010 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Feb 19 20:41:34 2010 +0100
@@ -641,8 +641,7 @@
       |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
       |> Sign.declare_const ((Binding.conceal binding, predT), NoSyn) |> snd
       |> PureThy.add_defs false
-        [((Binding.conceal (Binding.map_name Thm.def_name binding),
-            Logic.mk_equals (head, body)), [])];
+        [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
     val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
 
     val cert = Thm.cterm_of defs_thy;
diff -r b625eb708d94 -r 18ae6ef02fe0 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Feb 19 20:39:48 2010 +0100
+++ b/src/Pure/axclass.ML	Fri Feb 19 20:41:34 2010 +0100
@@ -474,7 +474,7 @@
     val ([def], def_thy) =
       thy
       |> Sign.primitive_class (bclass, super)
-      |> PureThy.add_defs false [((Binding.map_name Thm.def_name bconst, class_eq), [])];
+      |> PureThy.add_defs false [((Thm.def_binding bconst, class_eq), [])];
     val (raw_intro, (raw_classrel, raw_axioms)) =
       split_defined (length conjs) def ||> chop (length super);
 
diff -r b625eb708d94 -r 18ae6ef02fe0 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Fri Feb 19 20:39:48 2010 +0100
+++ b/src/Pure/more_thm.ML	Fri Feb 19 20:41:34 2010 +0100
@@ -77,6 +77,7 @@
   val untag: string -> attribute
   val def_name: string -> string
   val def_name_optional: string -> string -> string
+  val def_binding: Binding.binding -> Binding.binding
   val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding
   val has_name_hint: thm -> bool
   val get_name_hint: thm -> string
@@ -384,8 +385,10 @@
 fun def_name_optional c "" = def_name c
   | def_name_optional _ name = name;
 
+val def_binding = Binding.map_name def_name;
+
 fun def_binding_optional b name =
-  if Binding.is_empty name then Binding.map_name def_name b else name;
+  if Binding.is_empty name then def_binding b else name;
 
 
 (* unofficial theorem names *)