1.1 --- a/doc-src/more_antiquote.ML	Mon May 31 19:36:13 2010 +0200
     1.2 +++ b/doc-src/more_antiquote.ML	Mon May 31 21:06:57 2010 +0200
     1.3 @@ -64,8 +64,8 @@
     1.4  
     1.5  in
     1.6  
     1.7 -val _ = ThyOutput.antiquotation "class" (Scan.lift Args.name) (pr_class o #context);
     1.8 -val _ = ThyOutput.antiquotation "type" (Scan.lift Args.name) (pr_type o #context);
     1.9 +val _ = Thy_Output.antiquotation "class" (Scan.lift Args.name) (pr_class o #context);
    1.10 +val _ = Thy_Output.antiquotation "type" (Scan.lift Args.name) (pr_type o #context);
    1.11  
    1.12  end;
    1.13  
    1.14 @@ -95,11 +95,11 @@
    1.15        |> snd
    1.16        |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
    1.17        |> map (holize o no_vars ctxt o AxClass.overload thy);
    1.18 -  in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end;
    1.19 +  in Thy_Output.output (Thy_Output.maybe_pretty_source (pretty_thm ctxt) src thms) end;
    1.20  
    1.21  in
    1.22  
    1.23 -val _ = ThyOutput.antiquotation "code_thms" Args.term
    1.24 +val _ = Thy_Output.antiquotation "code_thms" Args.term
    1.25    (fn {source, context, ...} => pretty_code_thm source context);
    1.26  
    1.27  end;
    1.28 @@ -123,7 +123,7 @@
    1.29  
    1.30  in
    1.31  
    1.32 -val _ = ThyOutput.antiquotation "code_stmts"
    1.33 +val _ = Thy_Output.antiquotation "code_stmts"
    1.34    (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
    1.35    (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
    1.36      let val thy = ProofContext.theory_of ctxt in