Thm.def_binding;
authorwenzelm
Fri Feb 19 20:41:34 2010 +0100 (2010-02-19)
changeset 3523818ae6ef02fe0
parent 35237 b625eb708d94
child 35239 0dfec017bc83
Thm.def_binding;
src/HOL/Tools/typedef.ML
src/Pure/Isar/expression.ML
src/Pure/axclass.ML
src/Pure/more_thm.ML
     1.1 --- a/src/HOL/Tools/typedef.ML	Fri Feb 19 20:39:48 2010 +0100
     1.2 +++ b/src/HOL/Tools/typedef.ML	Fri Feb 19 20:41:34 2010 +0100
     1.3 @@ -119,8 +119,7 @@
     1.4        if def then
     1.5          theory
     1.6          |> Sign.add_consts_i [(name, setT', NoSyn)]   (* FIXME authentic syntax *)
     1.7 -        |> PureThy.add_defs false
     1.8 -          [((Binding.map_name Thm.def_name name, Logic.mk_equals (setC, set)), [])]
     1.9 +        |> PureThy.add_defs false [((Thm.def_binding name, Logic.mk_equals (setC, set)), [])]
    1.10          |-> (fn [th] => pair (SOME th))
    1.11        else (NONE, theory);
    1.12      fun contract_def NONE th = th
     2.1 --- a/src/Pure/Isar/expression.ML	Fri Feb 19 20:39:48 2010 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Fri Feb 19 20:41:34 2010 +0100
     2.3 @@ -641,8 +641,7 @@
     2.4        |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
     2.5        |> Sign.declare_const ((Binding.conceal binding, predT), NoSyn) |> snd
     2.6        |> PureThy.add_defs false
     2.7 -        [((Binding.conceal (Binding.map_name Thm.def_name binding),
     2.8 -            Logic.mk_equals (head, body)), [])];
     2.9 +        [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
    2.10      val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
    2.11  
    2.12      val cert = Thm.cterm_of defs_thy;
     3.1 --- a/src/Pure/axclass.ML	Fri Feb 19 20:39:48 2010 +0100
     3.2 +++ b/src/Pure/axclass.ML	Fri Feb 19 20:41:34 2010 +0100
     3.3 @@ -474,7 +474,7 @@
     3.4      val ([def], def_thy) =
     3.5        thy
     3.6        |> Sign.primitive_class (bclass, super)
     3.7 -      |> PureThy.add_defs false [((Binding.map_name Thm.def_name bconst, class_eq), [])];
     3.8 +      |> PureThy.add_defs false [((Thm.def_binding bconst, class_eq), [])];
     3.9      val (raw_intro, (raw_classrel, raw_axioms)) =
    3.10        split_defined (length conjs) def ||> chop (length super);
    3.11  
     4.1 --- a/src/Pure/more_thm.ML	Fri Feb 19 20:39:48 2010 +0100
     4.2 +++ b/src/Pure/more_thm.ML	Fri Feb 19 20:41:34 2010 +0100
     4.3 @@ -77,6 +77,7 @@
     4.4    val untag: string -> attribute
     4.5    val def_name: string -> string
     4.6    val def_name_optional: string -> string -> string
     4.7 +  val def_binding: Binding.binding -> Binding.binding
     4.8    val def_binding_optional: Binding.binding -> Binding.binding -> Binding.binding
     4.9    val has_name_hint: thm -> bool
    4.10    val get_name_hint: thm -> string
    4.11 @@ -384,8 +385,10 @@
    4.12  fun def_name_optional c "" = def_name c
    4.13    | def_name_optional _ name = name;
    4.14  
    4.15 +val def_binding = Binding.map_name def_name;
    4.16 +
    4.17  fun def_binding_optional b name =
    4.18 -  if Binding.is_empty name then Binding.map_name def_name b else name;
    4.19 +  if Binding.is_empty name then def_binding b else name;
    4.20  
    4.21  
    4.22  (* unofficial theorem names *)