# HG changeset patch
# User wenzelm
# Date 1212441129 -7200
# Node ID 51c2635dd89cb773c39634f8afd81dcc8ab57387
# Parent  4e7ecec1b685618db4e50a351cf5b5aaad5a2cc2
updated ML types for advanced translations;

diff -r 4e7ecec1b685 -r 51c2635dd89c doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Mon Jun 02 23:11:51 2008 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Mon Jun 02 23:12:09 2008 +0200
@@ -4,7 +4,7 @@
 imports Main
 begin
 
-chapter {* Specifications *}
+chapter {* Theory specifications *}
 
 section {* Defining theories \label{sec:begin-thy} *}
 
@@ -1102,7 +1102,7 @@
   \begin{matharray}{rcll}
     @{command_def "axioms"} & : & \isartrans{theory}{theory} & (axiomatic!) \\
     @{command_def "lemmas"} & : & \isarkeep{local{\dsh}theory} \\
-    @{command_def "theorems"} & : & isarkeep{local{\dsh}theory} \\
+    @{command_def "theorems"} & : & \isarkeep{local{\dsh}theory} \\
   \end{matharray}
 
   \begin{rail}
@@ -1319,15 +1319,15 @@
 %FIXME proper antiquotations
 \begin{ttbox}
 val parse_ast_translation:
-  (string * (Context.generic -> ast list -> ast)) list
+  (string * (Proof.context -> ast list -> ast)) list
 val parse_translation:
-  (string * (Context.generic -> term list -> term)) list
+  (string * (Proof.context -> term list -> term)) list
 val print_translation:
-  (string * (Context.generic -> term list -> term)) list
+  (string * (Proof.context -> term list -> term)) list
 val typed_print_translation:
-  (string * (Context.generic -> bool -> typ -> term list -> term)) list
+  (string * (Proof.context -> bool -> typ -> term list -> term)) list
 val print_ast_translation:
-  (string * (Context.generic -> ast list -> ast)) list
+  (string * (Proof.context -> ast list -> ast)) list
 \end{ttbox}
 *}