--- a/src/Pure/variable.ML Fri Apr 15 15:33:57 2011 +0200
+++ b/src/Pure/variable.ML Sat Apr 16 12:46:18 2011 +0200
@@ -19,6 +19,7 @@
val is_fixed: Proof.context -> string -> bool
val newly_fixed: Proof.context -> Proof.context -> string -> bool
val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
+ val name: binding -> string
val default_type: Proof.context -> string -> typ option
val def_type: Proof.context -> bool -> indexname -> typ option
val def_sort: Proof.context -> indexname -> sort option
@@ -155,6 +156,9 @@
fun add_fixed ctxt = Term.fold_aterms
(fn Free (x, T) => if is_fixed ctxt x then insert (op =) (x, T) else I | _ => I);
+(*checked name binding*)
+val name = Long_Name.base_name o Name_Space.full_name Name_Space.default_naming;
+
(** declarations **)