--- a/src/Pure/name.ML Thu Mar 06 10:12:47 2014 +0100
+++ b/src/Pure/name.ML Thu Mar 06 10:53:14 2014 +0100
@@ -14,9 +14,11 @@
val internal: string -> string
val dest_internal: string -> string
val is_internal: string -> bool
+ val reject_internal: string * Position.T list -> unit
val skolem: string -> string
val dest_skolem: string -> string
val is_skolem: string -> bool
+ val reject_skolem: string * Position.T list -> unit
val clean_index: string * int -> string * int
val clean: string -> string
type context
@@ -61,15 +63,19 @@
val is_bound = String.isPrefix ":";
-(* internal names *)
+(* internal names -- NB: internal subsumes skolem *)
val internal = suffix "_";
val dest_internal = unsuffix "_";
val is_internal = String.isSuffix "_";
+fun reject_internal (x, ps) =
+ if is_internal x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else ();
val skolem = suffix "__";
val dest_skolem = unsuffix "__";
val is_skolem = String.isSuffix "__";
+fun reject_skolem (x, ps) =
+ if is_skolem x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else ();
fun clean_index (x, i) =
(case try dest_internal x of