src/Pure/proofterm.ML
changeset 16536 c5744af6b28a
parent 16458 4c6fd0c01d28
child 16787 b6b6e2faaa41
     1.1 --- a/src/Pure/proofterm.ML	Wed Jun 22 19:41:20 2005 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Wed Jun 22 19:41:22 2005 +0200
     1.3 @@ -107,7 +107,7 @@
     1.4      (string * (typ list -> proof -> proof option)) list -> proof -> proof
     1.5    val rewrite_proof_notypes : (proof * proof) list *
     1.6      (string * (typ list -> proof -> proof option)) list -> proof -> proof
     1.7 -  val init : theory -> theory
     1.8 +  val init_data: theory -> theory
     1.9    
    1.10  end
    1.11  
    1.12 @@ -1107,7 +1107,7 @@
    1.13    fun print _ _ = ();
    1.14  end);
    1.15  
    1.16 -val init = ProofData.init;
    1.17 +val init_data = ProofData.init;
    1.18  
    1.19  fun add_prf_rrules rs thy =
    1.20    let val r = ProofData.get thy