src/Pure/Proof/proof_syntax.ML

     fun mk_term t = (if ty then I else map_types (K dummyT))
       (Term.no_dummy_patterns t);
 
     fun prf_of [] (Bound i) = PBound i
       | prf_of Ts (Const (s, Type ("Pure.proof", _))) =
-          Proofterm.change_type (if ty then SOME Ts else NONE)
+          Proofterm.change_types (if ty then SOME Ts else NONE)
             (case Long_Name.explode s of
                "axm" :: xs =>
                  let
                    val name = Long_Name.implode xs;
                    val prop = (case AList.lookup (op =) axms name of

                  end
              | _ => error ("Illegal proof constant name: " ^ quote s))
       | prf_of Ts (Const ("Pure.OfClass", _) $ Const (c_class, _)) =
           (case try Logic.class_of_const c_class of
             SOME c =>
-              Proofterm.change_type (if ty then SOME Ts else NONE)
+              Proofterm.change_types (if ty then SOME Ts else NONE)
                 (OfClass (TVar ((Name.aT, 0), []), c))
           | NONE => error ("Bad class constant: " ^ quote c_class))
       | prf_of Ts (Const ("Pure.Hyp", _) $ prop) = Hyp prop
       | prf_of Ts (v as Var ((_, Type ("Pure.proof", _)))) = Hyp v
       | prf_of [] (Const ("Pure.Abst", _) $ Abs (s, T, prf)) =