--- a/src/Pure/more_thm.ML Tue Dec 15 16:01:57 2015 +0100
+++ b/src/Pure/more_thm.ML Tue Dec 15 16:57:10 2015 +0100
@@ -97,6 +97,8 @@
val untag_rule: string -> thm -> thm
val tag: string * string -> attribute
val untag: string -> attribute
+ val is_free_dummy: thm -> bool
+ val tag_free_dummy: thm -> thm
val def_name: string -> string
val def_name_optional: string -> string -> string
val def_binding: Binding.binding -> Binding.binding
@@ -584,6 +586,13 @@
fun untag s = rule_attribute (K (untag_rule s));
+(* free dummy thm -- for abstract closure *)
+
+val free_dummyN = "free_dummy";
+fun is_free_dummy thm = Properties.defined (Thm.get_tags thm) free_dummyN;
+val tag_free_dummy = tag_rule (free_dummyN, "");
+
+
(* def_name *)
fun def_name c = c ^ "_def";