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 2821 c7d4bd9e89e0
parent 2819 4bd584ff4fab
child 2973 d1038e67923a 
--- a/Nominal/nominal_mutual.ML	Mon Jun 06 13:11:04 2011 +0100
+++ b/Nominal/nominal_mutual.ML	Tue Jun 07 08:52:59 2011 +0100
@@ -17,7 +17,7 @@
     -> term list
     -> local_theory
     -> ((thm (* goalstate *)
-        * (thm -> Nominal_Function_Common.function_result) (* proof continuation *)
+        * (thm -> Function_Common.function_result) (* proof continuation *)
        ) * local_theory)
 
 end
@@ -27,6 +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