1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu Feb 14 12:24:02 2002 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Feb 14 20:30:49 2002 +0100
     1.3 @@ -24,7 +24,7 @@
     1.4  
     1.5  (**** datatype definition ****)
     1.6  
     1.7 -fun add_dt_defs thy dep gr descr =
     1.8 +fun add_dt_defs thy dep gr (descr: DatatypeAux.descr) =
     1.9    let
    1.10      val sg = sign_of thy;
    1.11      val tab = DatatypePackage.get_datatypes thy;

     2.1 --- a/src/Pure/proofterm.ML	Thu Feb 14 12:24:02 2002 +0100
     2.2 +++ b/src/Pure/proofterm.ML	Thu Feb 14 20:30:49 2002 +0100
     2.3 @@ -16,8 +16,8 @@
     2.4       PBound of int
     2.5     | Abst of string * typ option * proof
     2.6     | AbsP of string * term option * proof
     2.7 -   | op % of proof * term option
     2.8 -   | op %% of proof * proof
     2.9 +   | % of proof * term option
    2.10 +   | %% of proof * proof
    2.11     | Hyp of term
    2.12     | PThm of (string * (string * string list) list) * proof * term * typ list option
    2.13     | PAxm of string * term * typ list option