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_function_core.ML
changeset 2796 3e341af86bbd
parent 2790 d2154b421707
child 2802 3b9ef98a03d2 
--- a/Nominal/nominal_function_core.ML	Tue May 31 14:12:31 2011 +0900
+++ b/Nominal/nominal_function_core.ML	Tue May 31 12:22:28 2011 +0100
@@ -336,7 +336,7 @@
     fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = 
         (llRI RS ih_eqvt_case)
         |> fold_rev (Thm.implies_intr o cprop_of) CCas
-        |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs
+        (* fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs *)
   in
     map prep_eqvt RCs
     |> map (fold_rev (Thm.implies_intr o cprop_of) ags)
nominal2