# HG changeset patch
# User wenzelm
# Date 1013715049 -3600
# Node ID 75b254b1c8bac19bb268d507edb56d92a9a83d9f
# Parent  1de4f0b824a8f14a4f451e410488d3e2a7395333
made MLWorks happy;

diff -r 1de4f0b824a8 -r 75b254b1c8ba src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Thu Feb 14 12:24:02 2002 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Thu Feb 14 20:30:49 2002 +0100
@@ -24,7 +24,7 @@
 
 (**** datatype definition ****)
 
-fun add_dt_defs thy dep gr descr =
+fun add_dt_defs thy dep gr (descr: DatatypeAux.descr) =
   let
     val sg = sign_of thy;
     val tab = DatatypePackage.get_datatypes thy;
diff -r 1de4f0b824a8 -r 75b254b1c8ba src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Feb 14 12:24:02 2002 +0100
+++ b/src/Pure/proofterm.ML	Thu Feb 14 20:30:49 2002 +0100
@@ -16,8 +16,8 @@
      PBound of int
    | Abst of string * typ option * proof
    | AbsP of string * term option * proof
-   | op % of proof * term option
-   | op %% of proof * proof
+   | % of proof * term option
+   | %% of proof * proof
    | Hyp of term
    | PThm of (string * (string * string list) list) * proof * term * typ list option
    | PAxm of string * term * typ list option