doc-src/more_antiquote.ML
changeset 29874 0b92f68124e8
parent 29619 82054da94a74
child 30202 2775062fd3a9
equal deleted inserted replaced
29856:984191be0357 29874:0b92f68124e8
    91 fun pretty_code_thm src ctxt raw_const =
    91 fun pretty_code_thm src ctxt raw_const =
    92   let
    92   let
    93     val thy = ProofContext.theory_of ctxt;
    93     val thy = ProofContext.theory_of ctxt;
    94     val const = Code_Unit.check_const thy raw_const;
    94     val const = Code_Unit.check_const thy raw_const;
    95     val (_, funcgr) = Code_Funcgr.make thy [const];
    95     val (_, funcgr) = Code_Funcgr.make thy [const];
       
    96     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
    96     val thms = Code_Funcgr.eqns funcgr const
    97     val thms = Code_Funcgr.eqns funcgr const
    97       |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    98       |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    98       |> map (no_vars ctxt o AxClass.overload thy);
    99       |> map (holize o no_vars ctxt o AxClass.overload thy);
    99   in ThyOutput.output_list pretty_thm src ctxt thms end;
   100   in ThyOutput.output_list pretty_thm src ctxt thms end;
   100 
   101 
   101 in
   102 in
   102 
   103 
   103 val _ = O.add_commands
   104 val _ = O.add_commands