--- 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;
--- 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