added scan_to_id (used to be in Pure/section_utils.ML);

--- a/src/HOL/thy_syntax.ML	Fri May 05 22:25:17 2000 +0200
+++ b/src/HOL/thy_syntax.ML	Fri May 05 22:29:02 2000 +0200
@@ -41,6 +41,14 @@
 
 (** (co)inductive **)
 
+(*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;
+
 fun inductive_decl coind =
   let
     val no_atts = map (mk_pair o rpair "[]");

--- 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 =