# HG changeset patch
# User berghofe
# Date 1014218038 -3600
# Node ID d3ad295a087a2d3f731c469ce38d8a3fc38b8d3d
# Parent  53bfe07a79164d80e8f1b244e40821d2ad4ca0cb
Moved change_type to proofterm.ML

diff -r 53bfe07a7916 -r d3ad295a087a 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;