Moved change_type to proofterm.ML
authorberghofe
Wed Feb 20 16:13:58 2002 +0100 (2002-02-20)
changeset 12909d3ad295a087a
parent 12908 53bfe07a7916
child 12910 f5bceeec9d91
Moved change_type to proofterm.ML
src/Pure/Proof/proof_syntax.ML
     1.1 --- a/src/Pure/Proof/proof_syntax.ML	Wed Feb 20 16:00:32 2002 +0100
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Wed Feb 20 16:13:58 2002 +0100
     1.3 @@ -121,10 +121,6 @@
     1.4  
     1.5  (**** translation between proof terms and pure terms ****)
     1.6  
     1.7 -fun change_type T (PThm (name, prf, prop, _)) = PThm (name, prf, prop, T)
     1.8 -  | change_type T (PAxm (name, prop, _)) = PAxm (name, prop, T)
     1.9 -  | change_type _ _ = error "Not a proper theorem";
    1.10 -
    1.11  fun proof_of_term thy tab ty =
    1.12    let
    1.13      val thys = thy :: Theory.ancestors_of thy;