src/Pure/more_thm.ML

 
 fun add_axiom (b, prop) thy =
   let
     val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
 
-    val _ = Sign.no_vars (Syntax.pp_global thy) prop;
+    val _ = Sign.no_vars (Syntax.init_pretty_global thy) prop;
     val (strip, recover, prop') = stripped_sorts thy prop;
     val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
     val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
 
     val thy' =

       |> fold elim_implies of_sorts;
   in ((axm_name, thm), thy') end;
 
 fun add_def unchecked overloaded (b, prop) thy =
   let
-    val _ = Sign.no_vars (Syntax.pp_global thy) prop;
+    val _ = Sign.no_vars (Syntax.init_pretty_global thy) prop;
     val prems = map (Thm.cterm_of thy) (Logic.strip_imp_prems prop);
     val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
 
     val thy' = Theory.add_def unchecked overloaded (b, concl') thy;
     val axm_name = Sign.full_name thy' b;