src/Pure/Proof/proof_syntax.ML
changeset 12909 d3ad295a087a
parent 11839 3ef83c265aca
child 13199 18402c1f76bf
     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;