--- a/doc-src/more_antiquote.ML Mon Mar 02 16:58:39 2009 +0100
+++ b/doc-src/more_antiquote.ML Mon Mar 02 16:58:39 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Doc/more_antiquote.ML
- ID: $Id$
Author: Florian Haftmann, TU Muenchen
More antiquotations.
@@ -92,9 +91,9 @@
let
val thy = ProofContext.theory_of ctxt;
val const = Code_Unit.check_const thy raw_const;
- val (_, funcgr) = Code_Funcgr.make thy [const];
+ val (_, funcgr) = Code_Wellsorted.make thy [const];
fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
- val thms = Code_Funcgr.eqns funcgr const
+ val thms = Code_Wellsorted.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_list pretty_thm src ctxt thms end;