src/Pure/theory.ML

        map (Sign.pretty_term sg) ts @
        map (Sign.pretty_typ sg o TVar) ixns)))));
 
 fun cert_axm sg (name, raw_tm) =
   let
-    val (t, T, _) = Sign.certify_term sg raw_tm
+    val (t, T, _) = Sign.certify_term (Sign.pp sg) sg raw_tm
       handle TYPE (msg, _, _) => error msg
            | TERM (msg, _) => error msg;
   in
     Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
     assert (T = propT) "Term not of type prop";

 
 (*some duplication of code with read_def_cterm*)
 fun read_def_axm (sg, types, sorts) used (name, str) =
   let
     val ts = Syntax.read (Sign.syn_of sg) propT str;
-    val (t, _) = Sign.infer_types sg types sorts used true (ts, propT);
+    val (t, _) = Sign.infer_types (Sign.pp sg) sg types sorts used true (ts, propT);
   in cert_axm sg (name, t) end
   handle ERROR => err_in_axm name;
 
 fun read_axm sg name_str = read_def_axm (sg, K None, K None) [] name_str;
 
 fun inferT_axm sg (name, pre_tm) =
-  let
-    val (t, _) = Sign.infer_types sg (K None) (K None) [] true ([pre_tm], propT);
+  let val (t, _) = Sign.infer_types (Sign.pp sg) sg
+    (K None) (K None) [] true ([pre_tm], propT);
   in (name, no_vars sg t) end
   handle ERROR => err_in_axm name;
 
 
 (* extend axioms of a theory *)

     make_theory sign const_deps final_consts' axioms oracles parents ancestors
   end;
 
 local
   fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT;
-  val cert_term = #1 oo Sign.certify_term;
+  fun cert_term sg = #1 o Sign.certify_term (Sign.pp sg) sg;
 in
 val add_finals = ext_finals read_term;
 val add_finals_i = ext_finals cert_term;
 end;