Function parse_theorem_scoped 

pub fn parse_theorem_scoped(
    ctx: &Context,
    scope: &Namespaces,
    input: &str,
) -> Result<(Command, usize), ParseError>

parse_theorem_in, reading every name in the namespace scope scope. The statement is reflected into syntax only after its names are resolved, so a theorem about add in a session that shadows add is a theorem about the session’s add.