Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_mutual.ML
changeset 2819 4bd584ff4fab
parent 2781 542ff50555f5
child 2821 c7d4bd9e89e0 
--- a/Nominal/nominal_mutual.ML	Sun Jun 05 16:58:18 2011 +0100
+++ b/Nominal/nominal_mutual.ML	Sun Jun 05 21:14:23 2011 +0100
@@ -11,13 +11,13 @@
 signature NOMINAL_FUNCTION_MUTUAL =
 sig
 
-  val prepare_nominal_function_mutual : Function_Common.function_config
+  val prepare_nominal_function_mutual : Nominal_Function_Common.nominal_function_config
     -> string (* defname *)
     -> ((string * typ) * mixfix) list
     -> term list
     -> local_theory
     -> ((thm (* goalstate *)
-        * (thm -> Function_Common.function_result) (* proof continuation *)
+        * (thm -> Nominal_Function_Common.function_result) (* proof continuation *)
        ) * local_theory)
 
 end
@@ -27,7 +27,7 @@
 struct
 
 open Function_Lib
-open Function_Common
+open Nominal_Function_Common
 
 type qgar = string * (string * typ) list * term list * term list * term
nominal2