# HG changeset patch
# User haftmann
# Date 1289989668 -3600
# Node ID 28cc2acbc58aab368e5e3e4f5cfe55c2bbed6912
# Parent  6fed6f9464717a1939b3511edc3f7462191d189e
ML signature interface

diff -r 6fed6f946471 -r 28cc2acbc58a src/HOL/Tools/functorial_mappers.ML
--- a/src/HOL/Tools/functorial_mappers.ML	Wed Nov 17 11:26:39 2010 +0100
+++ b/src/HOL/Tools/functorial_mappers.ML	Wed Nov 17 11:27:48 2010 +0100
@@ -11,6 +11,7 @@
     -> bool -> typ -> typ -> term
   val register: string -> string -> (sort * (bool * bool)) list -> thm -> thm
     -> theory -> theory
+  val type_mapper: term -> theory -> Proof.state
   type entry
   val entries: theory -> entry Symtab.table
 end;