src/HOL/thy_syntax.ML
changeset 8813 abc0f3722aed
parent 8657 b9475dad85ed
child 9857 2f994c499bef
     1.1 --- a/src/HOL/thy_syntax.ML	Fri May 05 22:25:17 2000 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Fri May 05 22:29:02 2000 +0200
     1.3 @@ -41,6 +41,14 @@
     1.4  
     1.5  (** (co)inductive **)
     1.6  
     1.7 +(*Skipping initial blanks, find the first identifier*)  (* FIXME slightly broken! *)
     1.8 +fun scan_to_id s =
     1.9 +    s |> Symbol.explode
    1.10 +    |> Scan.error (Scan.finite Symbol.stopper
    1.11 +      (Scan.!! (fn _ => "Expected to find an identifier in " ^ s)
    1.12 +        (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
    1.13 +    |> #1;
    1.14 +
    1.15  fun inductive_decl coind =
    1.16    let
    1.17      val no_atts = map (mk_pair o rpair "[]");