--- a/src/Pure/more_thm.ML Thu Jan 07 15:50:09 2016 +0100
+++ b/src/Pure/more_thm.ML Thu Jan 07 15:53:39 2016 +0100
@@ -92,6 +92,7 @@
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 make_def_binding: bool -> Binding.binding -> Binding.binding
val has_name_hint: thm -> bool
val get_name_hint: thm -> string
val put_name_hint: string -> thm -> thm
@@ -570,6 +571,9 @@
fun def_binding_optional b name =
if Binding.is_empty name then def_binding b else name;
+fun make_def_binding cond b =
+ if cond then Binding.reset_pos (def_binding b) else Binding.empty;
+
(* unofficial theorem names *)