1.1 --- a/doc-src/more_antiquote.ML	Thu Jan 08 08:06:11 2009 +0100
     1.2 +++ b/doc-src/more_antiquote.ML	Thu Jan 08 10:53:48 2009 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4    end
     1.5  
     1.6  
     1.7 -(* class antiquotation *)
     1.8 +(* class and type constructor antiquotation *)
     1.9  
    1.10  local
    1.11  
    1.12 @@ -74,6 +74,38 @@
    1.13  end;
    1.14  
    1.15  
    1.16 +(* code theorem antiquotation *)
    1.17 +
    1.18 +local
    1.19 +
    1.20 +fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
    1.21 +
    1.22 +fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
    1.23 +
    1.24 +fun no_vars ctxt thm =
    1.25 +  let
    1.26 +    val ctxt' = Variable.set_body false ctxt;
    1.27 +    val ((_, [thm]), _) = Variable.import_thms true [thm] ctxt';
    1.28 +  in thm end;
    1.29 +
    1.30 +fun pretty_code_thm src ctxt raw_const =
    1.31 +  let
    1.32 +    val thy = ProofContext.theory_of ctxt;
    1.33 +    val const = Code_Unit.check_const thy raw_const;
    1.34 +    val (_, funcgr) = Code_Funcgr.make thy [const];
    1.35 +    val thms = Code_Funcgr.eqns funcgr const
    1.36 +      |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    1.37 +      |> map (no_vars ctxt o AxClass.overload thy);
    1.38 +  in ThyOutput.output_list pretty_thm src ctxt thms end;
    1.39 +
    1.40 +in
    1.41 +
    1.42 +val _ = O.add_commands
    1.43 +  [("code_thms", ThyOutput.args Args.term pretty_code_thm)];
    1.44 +
    1.45 +end;
    1.46 +
    1.47 +
    1.48  (* code antiquotation *)
    1.49  
    1.50  local