# HG changeset patch
# User wenzelm
# Date 1158353768 -7200
# Node ID 796ae7fa10496c958c2514cf06b0adb51cbd15b4
# Parent  8923deb735ad3c449011f99a13f0003b5a3f1286
tuned;

diff -r 8923deb735ad -r 796ae7fa1049 doc-src/IsarImplementation/Thy/document/logic.tex
--- a/doc-src/IsarImplementation/Thy/document/logic.tex	Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Fri Sep 15 22:56:08 2006 +0200
@@ -134,6 +134,8 @@
   \indexmltype{typ}\verb|type typ| \\
   \indexml{map-atyps}\verb|map_atyps: (typ -> typ) -> typ -> typ| \\
   \indexml{fold-atyps}\verb|fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a| \\
+  \end{mldecls}
+  \begin{mldecls}
   \indexml{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
   \indexml{Sign.of-sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
   \indexml{Sign.add-types}\verb|Sign.add_types: (string * int * mixfix) list -> theory -> theory| \\
@@ -317,10 +319,12 @@
 \begin{mldecls}
   \indexmltype{term}\verb|type term| \\
   \indexml{op aconv}\verb|op aconv: term * term -> bool| \\
-  \indexml{map-term-types}\verb|map_term_types: (typ -> typ) -> term -> term| \\  %FIXME rename map_types
+  \indexml{map-types}\verb|map_types: (typ -> typ) -> term -> term| \\
   \indexml{fold-types}\verb|fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a| \\
   \indexml{map-aterms}\verb|map_aterms: (term -> term) -> term -> term| \\
   \indexml{fold-aterms}\verb|fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a| \\
+  \end{mldecls}
+  \begin{mldecls}
   \indexml{fastype-of}\verb|fastype_of: term -> typ| \\
   \indexml{lambda}\verb|lambda: term -> term -> term| \\
   \indexml{betapply}\verb|betapply: term * term -> term| \\
@@ -341,7 +345,7 @@
   on type \verb|term|; raw datatype equality should only be used
   for operations related to parsing or printing!
 
-  \item \verb|map_term_types|~\isa{f\ t} applies the mapping \isa{f} to all types occurring in \isa{t}.
+  \item \verb|map_types|~\isa{f\ t} applies the mapping \isa{f} to all types occurring in \isa{t}.
 
   \item \verb|fold_types|~\isa{f\ t} iterates the operation \isa{f} over all occurrences of types in \isa{t}; the term
   structure is traversed from left to right.
@@ -574,10 +578,12 @@
 \begin{mldecls}
   \indexmltype{ctyp}\verb|type ctyp| \\
   \indexmltype{cterm}\verb|type cterm| \\
+  \indexml{Thm.ctyp-of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
+  \indexml{Thm.cterm-of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
+  \end{mldecls}
+  \begin{mldecls}
   \indexmltype{thm}\verb|type thm| \\
   \indexml{proofs}\verb|proofs: int ref| \\
-  \indexml{Thm.ctyp-of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
-  \indexml{Thm.cterm-of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
   \indexml{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
   \indexml{Thm.forall-intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
   \indexml{Thm.forall-elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
@@ -587,6 +593,8 @@
   \indexml{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
   \indexml{Thm.get-axiom-i}\verb|Thm.get_axiom_i: theory -> string -> thm| \\
   \indexml{Thm.invoke-oracle-i}\verb|Thm.invoke_oracle_i: theory -> string -> theory * Object.T -> thm| \\
+  \end{mldecls}
+  \begin{mldecls}
   \indexml{Theory.add-axioms-i}\verb|Theory.add_axioms_i: (string * term) list -> theory -> theory| \\
   \indexml{Theory.add-deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
   \indexml{Theory.add-oracle}\verb|Theory.add_oracle: string * (theory * Object.T -> term) -> theory -> theory| \\
@@ -601,9 +609,13 @@
   well-typedness) checks, relative to the declarations of type
   constructors, constants etc. in the theory.
 
-  This representation avoids syntactic rechecking in tight loops of
-  inferences.  There are separate operations to decompose certified
-  entities (including actual theorems).
+  \item \verb|ctyp_of|~\isa{thy\ {\isasymtau}} and \verb|cterm_of|~\isa{thy\ t} explicitly checks types and terms, respectively.  This also
+  involves some basic normalizations, such expansion of type and term
+  abbreviations from the theory context.
+
+  Re-certification is relatively slow and should be avoided in tight
+  reasoning loops.  There are separate operations to decompose
+  certified entities (including actual theorems).
 
   \item \verb|thm| represents proven propositions.  This is an
   abstract datatype that guarantees that its values have been
diff -r 8923deb735ad -r 796ae7fa1049 doc-src/IsarImplementation/Thy/document/prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Fri Sep 15 22:56:08 2006 +0200
@@ -177,7 +177,9 @@
   \indexml{Theory.subthy}\verb|Theory.subthy: theory * theory -> bool| \\
   \indexml{Theory.merge}\verb|Theory.merge: theory * theory -> theory| \\
   \indexml{Theory.checkpoint}\verb|Theory.checkpoint: theory -> theory| \\
-  \indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\[1ex]
+  \indexml{Theory.copy}\verb|Theory.copy: theory -> theory| \\
+  \end{mldecls}
+  \begin{mldecls}
   \indexmltype{theory-ref}\verb|type theory_ref| \\
   \indexml{Theory.self-ref}\verb|Theory.self_ref: theory -> theory_ref| \\
   \indexml{Theory.deref}\verb|Theory.deref: theory_ref -> theory| \\
@@ -555,7 +557,9 @@
   \indexml{Symbol.is-letter}\verb|Symbol.is_letter: Symbol.symbol -> bool| \\
   \indexml{Symbol.is-digit}\verb|Symbol.is_digit: Symbol.symbol -> bool| \\
   \indexml{Symbol.is-quasi}\verb|Symbol.is_quasi: Symbol.symbol -> bool| \\
-  \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\[1ex]
+  \indexml{Symbol.is-blank}\verb|Symbol.is_blank: Symbol.symbol -> bool| \\
+  \end{mldecls}
+  \begin{mldecls}
   \indexmltype{Symbol.sym}\verb|type Symbol.sym| \\
   \indexml{Symbol.decode}\verb|Symbol.decode: Symbol.symbol -> Symbol.sym| \\
   \end{mldecls}
@@ -634,7 +638,9 @@
 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexml{Name.internal}\verb|Name.internal: string -> string| \\
-  \indexml{Name.skolem}\verb|Name.skolem: string -> string| \\[1ex]
+  \indexml{Name.skolem}\verb|Name.skolem: string -> string| \\
+  \end{mldecls}
+  \begin{mldecls}
   \indexmltype{Name.context}\verb|type Name.context| \\
   \indexml{Name.context}\verb|Name.context: Name.context| \\
   \indexml{Name.declare}\verb|Name.declare: string -> Name.context -> Name.context| \\
@@ -805,11 +811,15 @@
   \indexml{NameSpace.qualifier}\verb|NameSpace.qualifier: string -> string| \\
   \indexml{NameSpace.append}\verb|NameSpace.append: string -> string -> string| \\
   \indexml{NameSpace.pack}\verb|NameSpace.pack: string list -> string| \\
-  \indexml{NameSpace.unpack}\verb|NameSpace.unpack: string -> string list| \\[1ex]
+  \indexml{NameSpace.unpack}\verb|NameSpace.unpack: string -> string list| \\
+  \end{mldecls}
+  \begin{mldecls}
   \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
   \indexml{NameSpace.default-naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
   \indexml{NameSpace.add-path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
-  \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\[1ex]
+  \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\
+  \end{mldecls}
+  \begin{mldecls}
   \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
   \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
   \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
diff -r 8923deb735ad -r 796ae7fa1049 doc-src/IsarImplementation/Thy/document/proof.tex
--- a/doc-src/IsarImplementation/Thy/document/proof.tex	Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Fri Sep 15 22:56:08 2006 +0200
@@ -329,10 +329,14 @@
   \indexml{SUBPROOF}\verb|SUBPROOF: ({context: Proof.context, schematics: ctyp list * cterm list,|\isasep\isanewline%
 \verb|    params: cterm list, asms: cterm list, concl: cterm,|\isasep\isanewline%
 \verb|    prems: thm list} -> tactic) -> Proof.context -> int -> tactic| \\
+  \end{mldecls}
+  \begin{mldecls}
   \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
 \verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
   \indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
 \verb|  ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
+  \end{mldecls}
+  \begin{mldecls}
   \indexml{Obtain.result}\verb|Obtain.result: (Proof.context -> tactic) ->|\isasep\isanewline%
 \verb|  thm list -> Proof.context -> (cterm list * thm list) * Proof.context| \\
   \end{mldecls}
diff -r 8923deb735ad -r 796ae7fa1049 doc-src/IsarImplementation/Thy/document/tactic.tex
--- a/doc-src/IsarImplementation/Thy/document/tactic.tex	Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/tactic.tex	Fri Sep 15 22:56:08 2006 +0200
@@ -76,7 +76,7 @@
 
   \[
   \infer[\isa{{\isacharparenleft}init{\isacharparenright}}]{\isa{C\ {\isasymLongrightarrow}\ {\isacharhash}C}}{} \qquad
-  \infer[\isa{{\isacharparenleft}finish{\isacharparenright}}]{\isa{{\isacharhash}C}}{\isa{C}}
+  \infer[\isa{{\isacharparenleft}finish{\isacharparenright}}]{\isa{C}}{\isa{{\isacharhash}C}}
   \]
 
   \medskip The following low-level variants admit general reasoning
diff -r 8923deb735ad -r 796ae7fa1049 doc-src/IsarImplementation/Thy/logic.thy
--- a/doc-src/IsarImplementation/Thy/logic.thy	Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Fri Sep 15 22:56:08 2006 +0200
@@ -123,6 +123,8 @@
   @{index_ML_type typ} \\
   @{index_ML map_atyps: "(typ -> typ) -> typ -> typ"} \\
   @{index_ML fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
+  \end{mldecls}
+  \begin{mldecls}
   @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
   @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
   @{index_ML Sign.add_types: "(string * int * mixfix) list -> theory -> theory"} \\
@@ -315,10 +317,12 @@
   \begin{mldecls}
   @{index_ML_type term} \\
   @{index_ML "op aconv": "term * term -> bool"} \\
-  @{index_ML map_term_types: "(typ -> typ) -> term -> term"} \\  %FIXME rename map_types
+  @{index_ML map_types: "(typ -> typ) -> term -> term"} \\
   @{index_ML fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   @{index_ML map_aterms: "(term -> term) -> term -> term"} \\
   @{index_ML fold_aterms: "(term -> 'a -> 'a) -> term -> 'a -> 'a"} \\
+  \end{mldecls}
+  \begin{mldecls}
   @{index_ML fastype_of: "term -> typ"} \\
   @{index_ML lambda: "term -> term -> term"} \\
   @{index_ML betapply: "term * term -> term"} \\
@@ -341,7 +345,7 @@
   on type @{ML_type term}; raw datatype equality should only be used
   for operations related to parsing or printing!
 
-  \item @{ML map_term_types}~@{text "f t"} applies the mapping @{text
+  \item @{ML map_types}~@{text "f t"} applies the mapping @{text
   "f"} to all types occurring in @{text "t"}.
 
   \item @{ML fold_types}~@{text "f t"} iterates the operation @{text
@@ -576,10 +580,12 @@
   \begin{mldecls}
   @{index_ML_type ctyp} \\
   @{index_ML_type cterm} \\
+  @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
+  @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
+  \end{mldecls}
+  \begin{mldecls}
   @{index_ML_type thm} \\
   @{index_ML proofs: "int ref"} \\
-  @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
-  @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
   @{index_ML Thm.assume: "cterm -> thm"} \\
   @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
   @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
@@ -589,6 +595,8 @@
   @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
   @{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
   @{index_ML Thm.invoke_oracle_i: "theory -> string -> theory * Object.T -> thm"} \\
+  \end{mldecls}
+  \begin{mldecls}
   @{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
   @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
   @{index_ML Theory.add_oracle: "string * (theory * Object.T -> term) -> theory -> theory"} \\
@@ -603,9 +611,14 @@
   well-typedness) checks, relative to the declarations of type
   constructors, constants etc. in the theory.
 
-  This representation avoids syntactic rechecking in tight loops of
-  inferences.  There are separate operations to decompose certified
-  entities (including actual theorems).
+  \item @{ML ctyp_of}~@{text "thy \<tau>"} and @{ML cterm_of}~@{text "thy
+  t"} explicitly checks types and terms, respectively.  This also
+  involves some basic normalizations, such expansion of type and term
+  abbreviations from the theory context.
+
+  Re-certification is relatively slow and should be avoided in tight
+  reasoning loops.  There are separate operations to decompose
+  certified entities (including actual theorems).
 
   \item @{ML_type thm} represents proven propositions.  This is an
   abstract datatype that guarantees that its values have been
diff -r 8923deb735ad -r 796ae7fa1049 doc-src/IsarImplementation/Thy/prelim.thy
--- a/doc-src/IsarImplementation/Thy/prelim.thy	Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/prelim.thy	Fri Sep 15 22:56:08 2006 +0200
@@ -152,7 +152,9 @@
   @{index_ML Theory.subthy: "theory * theory -> bool"} \\
   @{index_ML Theory.merge: "theory * theory -> theory"} \\
   @{index_ML Theory.checkpoint: "theory -> theory"} \\
-  @{index_ML Theory.copy: "theory -> theory"} \\[1ex]
+  @{index_ML Theory.copy: "theory -> theory"} \\
+  \end{mldecls}
+  \begin{mldecls}
   @{index_ML_type theory_ref} \\
   @{index_ML Theory.self_ref: "theory -> theory_ref"} \\
   @{index_ML Theory.deref: "theory_ref -> theory"} \\
@@ -480,7 +482,9 @@
   @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
   @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
   @{index_ML Symbol.is_quasi: "Symbol.symbol -> bool"} \\
-  @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\[1ex]
+  @{index_ML Symbol.is_blank: "Symbol.symbol -> bool"} \\
+  \end{mldecls}
+  \begin{mldecls}
   @{index_ML_type "Symbol.sym"} \\
   @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
   \end{mldecls}
@@ -552,7 +556,9 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML Name.internal: "string -> string"} \\
-  @{index_ML Name.skolem: "string -> string"} \\[1ex]
+  @{index_ML Name.skolem: "string -> string"} \\
+  \end{mldecls}
+  \begin{mldecls}
   @{index_ML_type Name.context} \\
   @{index_ML Name.context: Name.context} \\
   @{index_ML Name.declare: "string -> Name.context -> Name.context"} \\
@@ -697,11 +703,15 @@
   @{index_ML NameSpace.qualifier: "string -> string"} \\
   @{index_ML NameSpace.append: "string -> string -> string"} \\
   @{index_ML NameSpace.pack: "string list -> string"} \\
-  @{index_ML NameSpace.unpack: "string -> string list"} \\[1ex]
+  @{index_ML NameSpace.unpack: "string -> string list"} \\
+  \end{mldecls}
+  \begin{mldecls}
   @{index_ML_type NameSpace.naming} \\
   @{index_ML NameSpace.default_naming: NameSpace.naming} \\
   @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
-  @{index_ML NameSpace.full: "NameSpace.naming -> string -> string"} \\[1ex]
+  @{index_ML NameSpace.full: "NameSpace.naming -> string -> string"} \\
+  \end{mldecls}
+  \begin{mldecls}
   @{index_ML_type NameSpace.T} \\
   @{index_ML NameSpace.empty: NameSpace.T} \\
   @{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\
diff -r 8923deb735ad -r 796ae7fa1049 doc-src/IsarImplementation/Thy/proof.thy
--- a/doc-src/IsarImplementation/Thy/proof.thy	Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy	Fri Sep 15 22:56:08 2006 +0200
@@ -290,10 +290,14 @@
   "({context: Proof.context, schematics: ctyp list * cterm list,
     params: cterm list, asms: cterm list, concl: cterm,
     prems: thm list} -> tactic) -> Proof.context -> int -> tactic"} \\
+  \end{mldecls}
+  \begin{mldecls}
   @{index_ML Goal.prove: "Proof.context -> string list -> term list -> term ->
   ({prems: thm list, context: Proof.context} -> tactic) -> thm"} \\
   @{index_ML Goal.prove_multi: "Proof.context -> string list -> term list -> term list ->
   ({prems: thm list, context: Proof.context} -> tactic) -> thm list"} \\
+  \end{mldecls}
+  \begin{mldecls}
   @{index_ML Obtain.result: "(Proof.context -> tactic) ->
   thm list -> Proof.context -> (cterm list * thm list) * Proof.context"} \\
   \end{mldecls}
diff -r 8923deb735ad -r 796ae7fa1049 doc-src/IsarImplementation/Thy/tactic.thy
--- a/doc-src/IsarImplementation/Thy/tactic.thy	Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/tactic.thy	Fri Sep 15 22:56:08 2006 +0200
@@ -61,7 +61,7 @@
 
   \[
   \infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad
-  \infer[@{text "(finish)"}]{@{text "#C"}}{@{text "C"}}
+  \infer[@{text "(finish)"}]{@{text "C"}}{@{text "#C"}}
   \]
 
   \medskip The following low-level variants admit general reasoning
diff -r 8923deb735ad -r 796ae7fa1049 doc-src/IsarImplementation/style.sty
--- a/doc-src/IsarImplementation/style.sty	Fri Sep 15 20:08:38 2006 +0200
+++ b/doc-src/IsarImplementation/style.sty	Fri Sep 15 22:56:08 2006 +0200
@@ -37,7 +37,7 @@
 
 \renewcommand{\isadigit}[1]{\isamath{#1}}
 
-\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\medskip\endgroup}
+\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
 
 \isafoldtag{FIXME}
 \isakeeptag{mlref}
diff -r 8923deb735ad -r 796ae7fa1049 src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Fri Sep 15 20:08:38 2006 +0200
+++ b/src/HOL/Algebra/ringsimp.ML	Fri Sep 15 22:56:08 2006 +0200
@@ -8,7 +8,7 @@
 signature ALGEBRA =
 sig
   val print_structures: Context.generic -> unit
-  val setup: Theory.theory -> Theory.theory
+  val setup: theory -> theory
 end;
 
 structure Algebra: ALGEBRA =
@@ -17,7 +17,7 @@
 
 (** Theory and context data **)
 
-fun struct_eq ((s1, ts1), (s2, ts2)) =
+fun struct_eq ((s1: string, ts1), (s2, ts2)) =
   (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
 
 structure AlgebraData = GenericDataFun
diff -r 8923deb735ad -r 796ae7fa1049 src/HOL/Real/Float.ML
--- a/src/HOL/Real/Float.ML	Fri Sep 15 20:08:38 2006 +0200
+++ b/src/HOL/Real/Float.ML	Fri Sep 15 22:56:08 2006 +0200
@@ -458,7 +458,7 @@
 			 end
 		       | _ => raise exn
 		    )
-val th = ref ([]: Theory.theory list)
+val th = ref ([]: theory list)
 val sg = ref ([]: Sign.sg list)
 
 fun invoke_float_op c = 
@@ -507,4 +507,4 @@
 	invoke_oracle th "nat_op" (sg, Nat_op_oracle_data c)
     end
 *)
-end;
\ No newline at end of file
+end;
diff -r 8923deb735ad -r 796ae7fa1049 src/HOL/Tools/cnf_funcs.ML
--- a/src/HOL/Tools/cnf_funcs.ML	Fri Sep 15 20:08:38 2006 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML	Fri Sep 15 22:56:08 2006 +0200
@@ -42,8 +42,8 @@
 
 	val weakening_tac : int -> Tactical.tactic  (* removes the first hypothesis of a subgoal *)
 
-	val make_cnf_thm  : Theory.theory -> Term.term -> Thm.thm
-	val make_cnfx_thm : Theory.theory -> Term.term ->  Thm.thm
+	val make_cnf_thm  : theory -> Term.term -> Thm.thm
+	val make_cnfx_thm : theory -> Term.term ->  Thm.thm
 	val cnf_rewrite_tac  : int -> Tactical.tactic  (* converts all prems of a subgoal to CNF *)
 	val cnfx_rewrite_tac : int -> Tactical.tactic  (* converts all prems of a subgoal to (almost) definitional CNF *)
 end;
@@ -176,8 +176,6 @@
 (* inst_thm: instantiates a theorem with a list of terms                     *)
 (* ------------------------------------------------------------------------- *)
 
-(* Theory.theory -> Term.term list -> Thm.thm -> Thm.thm *)
-
 fun inst_thm thy ts thm =
 	instantiate' [] (map (SOME o cterm_of thy) ts) thm;
 
diff -r 8923deb735ad -r 796ae7fa1049 src/HOL/Tools/res_atpset.ML
--- a/src/HOL/Tools/res_atpset.ML	Fri Sep 15 20:08:38 2006 +0200
+++ b/src/HOL/Tools/res_atpset.ML	Fri Sep 15 22:56:08 2006 +0200
@@ -84,7 +84,7 @@
   val extend = copy;
   fun merge _ (ref atpst1, ref atpst2) =
       ref (merge_atpset (atpst1, atpst2));
-  fun print (thy: Theory.theory) (ref atpst) = print_atpset atpst;
+  fun print _ (ref atpst) = print_atpset atpst;
 end);
 
 val print_AtpSet = GlobalAtpSet.print; 
@@ -138,4 +138,4 @@
 
 val setup = GlobalAtpSet.init #> LocalAtpSet.init #> setup_attrs;
 
-end;
\ No newline at end of file
+end;