diff -r 44637646fa17 -r 0e8e8903ff4e doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Fri Apr 24 21:27:49 2009 +0200
+++ b/doc-src/more_antiquote.ML	Sat Apr 25 08:34:30 2009 +0200
@@ -88,7 +88,7 @@
   let
     val thy = ProofContext.theory_of ctxt;
     val const = Code_Unit.check_const thy raw_const;
-    val (_, funcgr) = Code_Wellsorted.make thy [const];
+    val (_, funcgr) = Code_Wellsorted.obtain thy [const] [];
     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
     val thms = Code_Wellsorted.eqns funcgr const
       |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)