src/Pure/Proof/proof_syntax.ML

--- a/src/Pure/Proof/proof_syntax.ML	Wed Feb 20 16:00:32 2002 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Wed Feb 20 16:13:58 2002 +0100
@@ -121,10 +121,6 @@
 
 (**** 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;