src/Pure/codegen.ML

 fun set_iterations iterations ({size, default_type, ...} : test_params) =
   {size = size, iterations = iterations, default_type = default_type};
 
 fun set_default_type s thy ({size, iterations, ...} : test_params) =
   {size = size, iterations = iterations,
-   default_type = SOME (typ_of (read_ctyp thy s))};
+   default_type = SOME (Sign.read_typ thy s)};
 
 (* data kind 'Pure/codegen' *)
 
 structure CodegenData = TheoryDataFun
 (struct

          end
      | _ => error ("Not a constant: " ^ s))
   end) (thy, xs);
 
 val assoc_consts_i = gen_assoc_consts (K I);
-val assoc_consts = gen_assoc_consts (typ_of oo read_ctyp);
+val assoc_consts = gen_assoc_consts Sign.read_typ;
 
 
 (**** associate types with target language types ****)
 
 fun assoc_types xs thy = Library.foldl (fn (thy, (s, syn)) =>

 fun get_aux_code xs = map_filter (fn (m, code) =>
   if m = "" orelse member (op =) (!mode) m then SOME code else NONE) xs;
 
 fun mk_deftab thy =
   let
-    val axmss = map (fn thy' =>
-      (Context.theory_name thy', snd (#axioms (Theory.rep_theory thy'))))
+    val axmss = map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy'))
       (thy :: Theory.ancestors_of thy);
     fun prep_def def = (case preprocess thy [def] of
       [def'] => prop_of def' | _ => error "mk_deftab: bad preprocessor");
     fun dest t =
       let

            (output_code (fst gr') (if_library "" module) ["<Top>"]))
   in
     (code'', del_nodes ["<Top>"] gr')
   end));
 
-val generate_code_i = gen_generate_code (K I);
-val generate_code = gen_generate_code
-  (fn thy => term_of o read_cterm thy o rpair TypeInfer.logicT);
+val generate_code_i = gen_generate_code Sign.cert_term;
+val generate_code = gen_generate_code Sign.read_term;
 
 
 (**** Reflection ****)
 
 val strip_tname = implode o tl o explode;

   OuterSyntax.command "types_code"
   "associate types with target language types" K.thy_decl
     (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
      (fn xs => Toplevel.theory (fn thy => assoc_types
        (map (fn ((name, mfx), aux) => (name, (parse_mixfix
-         (typ_of o read_ctyp thy) mfx, aux))) xs) thy)));
+         (Sign.read_typ thy) mfx, aux))) xs) thy)));
 
 val assoc_constP =
   OuterSyntax.command "consts_code"
   "associate constants with target language code" K.thy_decl
     (Scan.repeat1
        (P.xname -- (Scan.option (P.$$$ "::" |-- P.typ)) --|
         P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
      (fn xs => Toplevel.theory (fn thy => assoc_consts
-       (map (fn (((name, optype), mfx), aux) => (name, optype, (parse_mixfix
-         (term_of o read_cterm thy o rpair TypeInfer.logicT) mfx, aux)))
-           xs) thy)));
+       (map (fn (((name, optype), mfx), aux) =>
+         (name, optype, (parse_mixfix (Sign.read_term thy) mfx, aux))) xs) thy)));
 
 fun parse_code lib =
   Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) --
   (if lib then Scan.optional P.name "" else P.name) --
   Scan.option (P.$$$ "file" |-- P.name) --

 val parse_test_params = P.short_ident :-- (fn s =>
   P.$$$ "=" |-- (AList.lookup (op =) params s |> the_default Scan.fail)) >> snd;
 
 fun parse_tyinst xs =
   (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
-    fn (x, ys) => (x, (v, typ_of (read_ctyp thy s)) :: ys))) xs;
+    fn (x, ys) => (x, (v, Sign.read_typ thy s) :: ys))) xs;
 
 fun app [] x = x
   | app (f :: fs) x = app fs (f x);
 
 val test_paramsP =