--- a/doc-src/IsarImplementation/Thy/logic.thy Sat Dec 06 08:45:38 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/logic.thy Sat Dec 06 08:57:39 2008 +0100
@@ -1,6 +1,3 @@
-
-(* $Id$ *)
-
theory logic imports base begin
chapter {* Primitive logic \label{ch:logic} *}
@@ -326,9 +323,9 @@
@{index_ML fastype_of: "term -> typ"} \\
@{index_ML lambda: "term -> term -> term"} \\
@{index_ML betapply: "term * term -> term"} \\
- @{index_ML Sign.declare_const: "Properties.T -> (Name.binding * typ) * mixfix ->
+ @{index_ML Sign.declare_const: "Properties.T -> (Binding.T * typ) * mixfix ->
theory -> term * theory"} \\
- @{index_ML Sign.add_abbrev: "string -> Properties.T -> Name.binding * term ->
+ @{index_ML Sign.add_abbrev: "string -> Properties.T -> Binding.T * term ->
theory -> (term * term) * theory"} \\
@{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
@{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\