1.1 --- a/doc-src/more_antiquote.ML	Thu May 14 15:09:47 2009 +0200
     1.2 +++ b/doc-src/more_antiquote.ML	Thu May 14 15:09:48 2009 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4  fun pretty_code_thm src ctxt raw_const =
     1.5    let
     1.6      val thy = ProofContext.theory_of ctxt;
     1.7 -    val const = Code_Unit.check_const thy raw_const;
     1.8 +    val const = Code.check_const thy raw_const;
     1.9      val (_, funcgr) = Code_Preproc.obtain thy [const] [];
    1.10      fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
    1.11      val thms = Code_Preproc.eqns funcgr const
    1.12 @@ -108,7 +108,7 @@
    1.13  local
    1.14  
    1.15    val parse_const_terms = Scan.repeat1 Args.term
    1.16 -    >> (fn ts => fn thy => map (Code_Unit.check_const thy) ts);
    1.17 +    >> (fn ts => fn thy => map (Code.check_const thy) ts);
    1.18    val parse_consts = Scan.lift (Args.parens (Args.$$$ "consts")) |-- parse_const_terms
    1.19      >> (fn mk_cs => fn thy => fn naming => map_filter (Code_Thingol.lookup_const naming) (mk_cs thy));
    1.20    val parse_types = Scan.lift (Args.parens (Args.$$$ "types") |-- Scan.repeat1 Args.name)