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 2975 c62e26830420
parent 2974 b95a2065aa10
child 2978 967c55907ce1 
--- a/Nominal/nominal_mutual.ML	Tue Jul 19 01:40:36 2011 +0100
+++ b/Nominal/nominal_mutual.ML	Tue Jul 19 02:30:05 2011 +0100
@@ -214,6 +214,8 @@
         val ctrm2 = f_def
           |> cprop_of
           |> Thm.dest_equals_lhs
+        val _ = tracing ("ctrm1:\n" ^ @{make_string} ctrm1)
+        val _ = tracing ("ctrm2:\n" ^ @{make_string} ctrm2)
       in
         eqvt_thm
 	|> Thm.instantiate (Thm.match (ctrm1, ctrm2))
nominal2