src/Pure/Thy/thy_syntax.scala
changeset 59689 7968c57ea240
parent 59684 86a76300137e
child 59695 a03e0561bdbf
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Mar 13 12:44:16 2015 +0100
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Mar 13 12:58:49 2015 +0100
     1.3 @@ -164,7 +164,7 @@
     1.4      val cmds0 = commands.iterator(first, last).toList
     1.5      val blobs_spans0 =
     1.6        syntax.parse_spans(cmds0.iterator.map(_.source).mkString).
     1.7 -        map(span => (Command_Span.resolve_files(resources, syntax, name, span, get_blob), span))
     1.8 +        map(span => (Command.resolve_files(resources, syntax, name, span, get_blob), span))
     1.9  
    1.10      val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)
    1.11