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