doc-src/more_antiquote.ML
changeset 31156 90fed3d4430f
parent 31143 2ce5c0c4d697
child 31794 71af1fd6a5e4
--- a/doc-src/more_antiquote.ML	Thu May 14 15:09:47 2009 +0200
+++ b/doc-src/more_antiquote.ML	Thu May 14 15:09:48 2009 +0200
@@ -87,7 +87,7 @@
 fun pretty_code_thm src ctxt raw_const =
   let
     val thy = ProofContext.theory_of ctxt;
-    val const = Code_Unit.check_const thy raw_const;
+    val const = Code.check_const thy raw_const;
     val (_, funcgr) = Code_Preproc.obtain thy [const] [];
     fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
     val thms = Code_Preproc.eqns funcgr const
@@ -108,7 +108,7 @@
 local
 
   val parse_const_terms = Scan.repeat1 Args.term
-    >> (fn ts => fn thy => map (Code_Unit.check_const thy) ts);
+    >> (fn ts => fn thy => map (Code.check_const thy) ts);
   val parse_consts = Scan.lift (Args.parens (Args.$$$ "consts")) |-- parse_const_terms
     >> (fn mk_cs => fn thy => fn naming => map_filter (Code_Thingol.lookup_const naming) (mk_cs thy));
   val parse_types = Scan.lift (Args.parens (Args.$$$ "types") |-- Scan.repeat1 Args.name)