src/Pure/Isar/parse.ML

   val thms1: (Facts.ref * Token.src list) list parser
   val options: ((string * Position.T) * (string * Position.T)) list parser
   val embedded_ml: ML_Lex.token Antiquote.antiquote list parser
   val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
   val read_embedded: Proof.context -> Keyword.keywords -> 'a parser -> Input.source -> 'a
-  val read_embedded_src: Proof.context -> Keyword.keywords -> 'a parser -> Token.src -> 'a
 end;
 
 structure Parse: PARSE =
 struct
 

     (case Scan.read Token.stopper parse toks of
       SOME res => res
     | NONE => error ("Bad input" ^ Position.here (Input.pos_of input)))
   end;
 
-fun read_embedded_src ctxt keywords parse src =
-  Token.read ctxt embedded_input src
-  |> read_embedded ctxt keywords parse;
-
 end;