src/Pure/Proof/proof_syntax.ML

   in (rename prf, tab) end;
 
 
 (**** translation between proof terms and pure terms ****)
 
-fun change_type T (PThm (name, prf, prop, _)) = PThm (name, prf, prop, T)
-  | change_type T (PAxm (name, prop, _)) = PAxm (name, prop, T)
-  | change_type _ _ = error "Not a proper theorem";
-
 fun proof_of_term thy tab ty =
   let
     val thys = thy :: Theory.ancestors_of thy;
     val thms = flat (map thms_of thys);
     val axms = flat (map (Symtab.dest o #axioms o rep_theory) thys);