1.1 --- a/doc-src/more_antiquote.ML Mon Mar 02 16:58:39 2009 +0100
1.2 +++ b/doc-src/more_antiquote.ML Mon Mar 02 16:58:39 2009 +0100
1.3 @@ -1,5 +1,4 @@
1.4 (* Title: Doc/more_antiquote.ML
1.5 - ID: $Id$
1.6 Author: Florian Haftmann, TU Muenchen
1.7
1.8 More antiquotations.
1.9 @@ -92,9 +91,9 @@
1.10 let
1.11 val thy = ProofContext.theory_of ctxt;
1.12 val const = Code_Unit.check_const thy raw_const;
1.13 - val (_, funcgr) = Code_Funcgr.make thy [const];
1.14 + val (_, funcgr) = Code_Wellsorted.make thy [const];
1.15 fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
1.16 - val thms = Code_Funcgr.eqns funcgr const
1.17 + val thms = Code_Wellsorted.eqns funcgr const
1.18 |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
1.19 |> map (holize o no_vars ctxt o AxClass.overload thy);
1.20 in ThyOutput.output_list pretty_thm src ctxt thms end;