Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
activating the signature of Predicate_Compile again which was deactivated in changeset d93a3cb55068 for debugging purposes
authorbulwahn
Wed, 31 Mar 2010 16:44:41 +0200
changeset 36050 88203782cf12
parent 36049 0ce5b7a5c2fd
child 36051 810357220388
activating the signature of Predicate_Compile again which was deactivated in changeset d93a3cb55068 for debugging purposes
src/HOL/Tools/Predicate_Compile/predicate_compile.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Mar 31 16:44:41 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Mar 31 16:44:41 2010 +0200
@@ -7,12 +7,12 @@
 signature PREDICATE_COMPILE =
 sig
   val setup : theory -> theory
-  val preprocess : Predicate_Compile_Aux.options -> string -> theory -> theory
+  val preprocess : Predicate_Compile_Aux.options -> term -> theory -> theory
   val present_graph : bool Unsynchronized.ref
   val intro_hook : (theory -> thm -> unit) option Unsynchronized.ref
 end;
 
-structure Predicate_Compile (*: PREDICATE_COMPILE*) =
+structure Predicate_Compile : PREDICATE_COMPILE =
 struct
 
 val present_graph = Unsynchronized.ref false
isabelle