diff -r 8f609d1e7002 -r 2ce5c0c4d697 doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Wed May 13 21:22:48 2009 +0200
+++ b/doc-src/more_antiquote.ML	Thu May 14 08:22:06 2009 +0200
@@ -88,9 +88,9 @@
   let
     val thy = ProofContext.theory_of ctxt;
     val const = Code_Unit.check_const thy raw_const;
-    val (_, funcgr) = Code_Wellsorted.obtain thy [const] [];
+    val (_, funcgr) = Code_Preproc.obtain thy [const] [];
     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
-    val thms = Code_Wellsorted.eqns funcgr const
+    val thms = Code_Preproc.eqns funcgr const
       |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
       |> map (holize o no_vars ctxt o AxClass.overload thy);
   in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end;