--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Feb 21 20:13:42 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Feb 22 14:28:05 2018 +0100
@@ -849,10 +849,9 @@
|> infer_instantiate' lthy (replicate live NONE @
[SOME (Thm.cterm_of lthy (ctorA $ y))])
|> unfold_thms lthy [dtor_ctor];
-
- val map_ctor_thm0 = fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans);
in
- Thm.generalize ([], [y_s]) (Thm.maxidx_of map_ctor_thm0 + 1) map_ctor_thm0
+ (fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans))
+ |> Drule.generalize ([], [y_s])
end;
val map_thms =
@@ -926,13 +925,12 @@
val ((y as Free (y_s, _), z as Free (z_s, _)), _) = lthy
|> yield_singleton (mk_Frees "y") y_T
||>> yield_singleton (mk_Frees "z") z_T;
-
- val rel_ctor_thm0 = fp_rel_thm
- |> infer_instantiate' lthy (replicate live NONE @
- [SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))])
- |> unfold_thms lthy [dtor_ctor];
in
- Thm.generalize ([], [y_s, z_s]) (Thm.maxidx_of rel_ctor_thm0 + 1) rel_ctor_thm0
+ fp_rel_thm
+ |> infer_instantiate' lthy (replicate live NONE @
+ [SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))])
+ |> unfold_thms lthy [dtor_ctor]
+ |> Drule.generalize ([], [y_s, z_s])
end;
val rel_inject_thms =