doc-src/more_antiquote.ML
changeset 30202 2775062fd3a9
parent 29874 0b92f68124e8
child 30394 c11a1e65a2ed
equal deleted inserted replaced
30201:39fefb3eedfc 30202:2775062fd3a9
     1 (*  Title:      Doc/more_antiquote.ML
     1 (*  Title:      Doc/more_antiquote.ML
     2     ID:         $Id$
       
     3     Author:     Florian Haftmann, TU Muenchen
     2     Author:     Florian Haftmann, TU Muenchen
     4 
     3 
     5 More antiquotations.
     4 More antiquotations.
     6 *)
     5 *)
     7 
     6 
    90 
    89 
    91 fun pretty_code_thm src ctxt raw_const =
    90 fun pretty_code_thm src ctxt raw_const =
    92   let
    91   let
    93     val thy = ProofContext.theory_of ctxt;
    92     val thy = ProofContext.theory_of ctxt;
    94     val const = Code_Unit.check_const thy raw_const;
    93     val const = Code_Unit.check_const thy raw_const;
    95     val (_, funcgr) = Code_Funcgr.make thy [const];
    94     val (_, funcgr) = Code_Wellsorted.make thy [const];
    96     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
    95     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
    97     val thms = Code_Funcgr.eqns funcgr const
    96     val thms = Code_Wellsorted.eqns funcgr const
    98       |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    97       |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    99       |> map (holize o no_vars ctxt o AxClass.overload thy);
    98       |> map (holize o no_vars ctxt o AxClass.overload thy);
   100   in ThyOutput.output_list pretty_thm src ctxt thms end;
    99   in ThyOutput.output_list pretty_thm src ctxt thms end;
   101 
   100 
   102 in
   101 in