# HG changeset patch # User wenzelm # Date 1268345232 -3600 # Node ID 9dd4747d95916386229c55cc95c26a0efdc3cd5c # Parent 9dc39bad4f4dab5afb24e4843972db92dd57143e tuned signature; diff -r 9dc39bad4f4d -r 9dd4747d9591 src/Pure/assumption.ML --- a/src/Pure/assumption.ML Thu Mar 11 23:07:02 2010 +0100 +++ b/src/Pure/assumption.ML Thu Mar 11 23:07:12 2010 +0100 @@ -6,7 +6,7 @@ signature ASSUMPTION = sig - type export + type export = bool -> cterm list -> (thm -> thm) * (term -> term) val assume_export: export val presume_export: export val assume: cterm -> thm