src/Doc/more_antiquote.ML
changeset 60697 e266d5463e9d
parent 56061 564a7bee8652
child 63026 9a9c2d846d4a
equal deleted inserted replaced
60696:8304fb4fb823 60697:e266d5463e9d
    23 
    23 
    24 fun pretty_code_thm src ctxt raw_const =
    24 fun pretty_code_thm src ctxt raw_const =
    25   let
    25   let
    26     val thy = Proof_Context.theory_of ctxt;
    26     val thy = Proof_Context.theory_of ctxt;
    27     val const = Code.check_const thy raw_const;
    27     val const = Code.check_const thy raw_const;
    28     val (_, eqngr) = Code_Preproc.obtain true thy [const] [];
    28     val (_, eqngr) = Code_Preproc.obtain true ctxt [const] [];
    29     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
    29     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
    30     val thms = Code_Preproc.cert eqngr const
    30     val thms = Code_Preproc.cert eqngr const
    31       |> Code.equations_of_cert thy
    31       |> Code.equations_of_cert thy
    32       |> snd
    32       |> snd
    33       |> these
    33       |> these