diff --git a/Logic/Makefile b/Logic/Makefile
index cdd328ce9..e0d722719 100644
--- a/Logic/Makefile
+++ b/Logic/Makefile
@@ -1,7 +1,7 @@
 PKG := TFF U Zenon PTS
 
 .PHONY: default
-default:
+default: clean
 	for p in $(PKG); do $(MAKE) -C $$p; done
 
 %:
diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml
index a7e5cc33e..426789863 100644
--- a/src/parsing/lpLexer.ml
+++ b/src/parsing/lpLexer.ml
@@ -153,7 +153,7 @@ let string = [%sedlex.regexp? '"', Star (Compl '"'), '"']
 
 (** Unqualified regular identifiers are any non-empty sequence of characters
    not among: *)
-let forbidden_letter = [%sedlex.regexp? Chars " ,;\r\t\n(){}[]:.`\"@$|?/*"]
+let forbidden_letter = [%sedlex.regexp? Chars " ,;\r\t\n(){}[]:.`\"@$|/"]
 let regid = [%sedlex.regexp? '/' | '*' | Plus (Compl forbidden_letter)]
 
 let is_regid : string -> bool = fun s ->
@@ -280,7 +280,7 @@ let rec token lb =
   | '_' -> UNDERSCORE
 
   (* identifiers *)
-  | regid -> UID(Utf8.lexeme lb)
+  | '/' | regid -> UID(Utf8.lexeme lb)
   | escid -> UID(remove_useless_escape(Utf8.lexeme lb))
   | '@', regid -> UID_EXPL(remove_first lb)
   | '@', escid -> UID_EXPL(remove_useless_escape(remove_first lb))
diff --git a/tests/OK/identifiers.lp b/tests/OK/identifiers.lp
new file mode 100644
index 000000000..394a5b9e7
--- /dev/null
+++ b/tests/OK/identifiers.lp
@@ -0,0 +1,3 @@
+symbol /:TYPE;
+symbol *:TYPE;
+symbol **:TYPE;