--- a/src/ZF/thy_syntax.ML Fri May 05 22:25:17 2000 +0200
+++ b/src/ZF/thy_syntax.ML Fri May 05 22:29:02 2000 +0200
@@ -27,6 +27,13 @@
|| list1 (name>>unenclose) >> mk_list))
"[]";
+(*Skipping initial blanks, find the first identifier*) (* FIXME slightly broken! *)
+fun scan_to_id s =
+ s |> Symbol.explode
+ |> Scan.error (Scan.finite Symbol.stopper
+ (Scan.!! (fn _ => "Expected to find an identifier in " ^ s)
+ (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
+ |> #1;
(*(Co)Inductive definitions theory section."*)
fun inductive_decl coind =