# HG changeset patch
# User wenzelm
# Date 1236782305 -3600
# Node ID 9b94b1358b959b42fe0e71c7a345f912a0b0a4f1
# Parent  ce5138c92ca74bc917251dfa55be4aceabd9abd3
Thm.def_binding_optional;

diff -r ce5138c92ca7 -r 9b94b1358b95 src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Wed Mar 11 15:36:12 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML	Wed Mar 11 15:38:25 2009 +0100
@@ -42,14 +42,15 @@
           if c <> c' then
             err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
           else ());
+    val b = Binding.name c;
 
     val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
-    val name = Binding.map_name (Thm.def_name_optional c) raw_name;
+    val name = Thm.def_binding_optional b raw_name;
     val atts = map (prep_att thy) raw_atts;
 
     val thy' =
       thy
-      |> Sign.add_consts_i [(Binding.name c, T, mx)]
+      |> Sign.add_consts_i [(b, T, mx)]
       |> PureThy.add_defs false [((name, def), atts)]
       |-> (fn [thm] => Code.add_default_eqn thm);
   in ((c, T), thy') end;
diff -r ce5138c92ca7 -r 9b94b1358b95 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Wed Mar 11 15:36:12 2009 +0100
+++ b/src/Pure/Isar/element.ML	Wed Mar 11 15:38:25 2009 +0100
@@ -502,7 +502,7 @@
         val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
         val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
             let val ((c, _), t') = LocalDefs.cert_def ctxt t
-            in (t', ((Binding.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
+            in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
         val (_, ctxt') =
           ctxt |> fold (Variable.auto_fixes o #1) asms
           |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
diff -r ce5138c92ca7 -r 9b94b1358b95 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Mar 11 15:36:12 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Mar 11 15:38:25 2009 +0100
@@ -304,7 +304,7 @@
             (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
         | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
             let val ((c, _), t') = LocalDefs.cert_def ctxt (close_frees t)
-            in ((Binding.map_name (Thm.def_name_optional c) name, atts), (t', no_binds ps)) end))
+            in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end))
         | e => e)
       end;
 
diff -r ce5138c92ca7 -r 9b94b1358b95 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Wed Mar 11 15:36:12 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML	Wed Mar 11 15:38:25 2009 +0100
@@ -91,7 +91,7 @@
     val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
     val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
     val xs = map Binding.name_of bvars;
-    val names = map2 (Binding.map_name o Thm.def_name_optional) xs bfacts;
+    val names = map2 Thm.def_binding_optional bvars bfacts;
     val eqs = mk_def ctxt (xs ~~ rhss);
     val lhss = map (fst o Logic.dest_equals) eqs;
   in
diff -r ce5138c92ca7 -r 9b94b1358b95 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Mar 11 15:36:12 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Wed Mar 11 15:38:25 2009 +0100
@@ -169,8 +169,7 @@
     val (vars, [((raw_name, atts), [prop])]) =
       fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy);
     val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
-    val name = Binding.map_name (Thm.def_name_optional x) raw_name;
-    val var =
+    val var as (b, _) =
       (case vars of
         [] => (Binding.name x, NoSyn)
       | [((b, _), mx)] =>
@@ -180,9 +179,12 @@
               error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.str_of (Binding.pos_of b));
           in (b, mx) end);
-    val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
+    val name = Thm.def_binding_optional b raw_name;
+    val ((lhs, (_, th)), lthy2) = lthy
+      |> LocalTheory.define Thm.definitionK
         (var, ((Binding.suffix_name "_raw" name, []), rhs));
-    val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
+    val ((def_name, [th']), lthy3) = lthy2
+      |> LocalTheory.note Thm.definitionK
         ((name, Code.add_default_eqn_attrib :: atts), [prove lthy2 th]);
 
     val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;