# HG changeset patch
# User wenzelm
# Date 1124192555 -7200
# Node ID 2fae6579fb2e6eb08f8e4f4e85dff3a9c522c875
# Parent  50210558395102b4a23df62ec268ef51808c1d26
added liberal_name;

diff -r 502105583951 -r 2fae6579fb2e src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Tue Aug 16 13:42:34 2005 +0200
+++ b/src/Pure/Isar/args.ML	Tue Aug 16 13:42:35 2005 +0200
@@ -47,6 +47,7 @@
   val maybe: (T list -> 'a * T list) -> T list -> 'a option * T list
   val name: T list -> string * T list
   val symbol: T list -> string * T list
+  val liberal_name: T list -> string * T list
   val nat: T list -> int * T list
   val int: T list -> int * T list
   val var: T list -> indexname * T list
@@ -251,6 +252,7 @@
 
 val name = named >> sym_of;
 val symbol = symbolic >> sym_of;
+val liberal_name = symbol || name;
 
 val nat = some_ident Syntax.read_nat;
 val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;