Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
made MLWorks happy;
authorwenzelm
Thu, 14 Feb 2002 20:30:49 +0100
changeset 12890 75b254b1c8ba
parent 12889 1de4f0b824a8
child 12891 92af5c3a10fb
made MLWorks happy;
src/HOL/Tools/datatype_codegen.ML file | annotate | diff | comparison | revisions
src/Pure/proofterm.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle