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)