1.1 --- a/doc-src/rail.ML	Mon May 31 19:36:13 2010 +0200
     1.2 +++ b/doc-src/rail.ML	Mon May 31 21:06:57 2010 +0200
     1.3 @@ -67,14 +67,14 @@
     1.4    ("fact", ("", no_check, true)),
     1.5    ("variable", ("", no_check, true)),
     1.6    ("case", ("", no_check, true)),
     1.7 -  ("antiquotation", ("", K ThyOutput.defined_command, true)),
     1.8 -  ("antiquotation option", ("", K ThyOutput.defined_option, true)), (* kann mein scanner nicht erkennen *)
     1.9 +  ("antiquotation", ("", K Thy_Output.defined_command, true)),
    1.10 +  ("antiquotation option", ("", K Thy_Output.defined_option, true)), (* kann mein scanner nicht erkennen *)
    1.11    ("setting", ("isatt", (fn _ => fn name => is_some (OS.Process.getEnv name)), true)),
    1.12    ("inference", ("", no_check, true)),
    1.13    ("executable", ("isatt", no_check, true)),
    1.14    ("tool", ("isatt", K check_tool, true)),
    1.15    ("file", ("isatt", K (File.exists o Path.explode), true)),
    1.16 -  ("theory", ("", K ThyInfo.known_thy, true))
    1.17 +  ("theory", ("", K Thy_Info.known_thy, true))
    1.18    ];
    1.19  
    1.20  in
    1.21 @@ -97,8 +97,8 @@
    1.22      (idx ^
    1.23      (Output.output name
    1.24        |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
    1.25 -      |> (if ! ThyOutput.quotes then quote else I)
    1.26 -      |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.27 +      |> (if ! Thy_Output.quotes then quote else I)
    1.28 +      |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.29            else hyper o enclose "\\mbox{\\isa{" "}}")), style)
    1.30    else ("Bad " ^ kind ^ " " ^ name, false)
    1.31    end;
    1.32 @@ -473,7 +473,7 @@
    1.33    |> parse
    1.34    |> print;
    1.35  
    1.36 -val _ = ThyOutput.antiquotation "rail" (Scan.lift (Parse.position Args.name))
    1.37 +val _ = Thy_Output.antiquotation "rail" (Scan.lift (Parse.position Args.name))
    1.38    (fn {context = ctxt,...} => fn txt => process txt ctxt);
    1.39  
    1.40  end;