summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 30 May 2015 20:21:53 +0200 | |

changeset 60313 | 2a0b42cd58fb |

parent 60312 | ee6f9a97205d |

child 60314 | 6e465f0d46d3 |

tuned -- more direct Thm.renamed_prop;

--- a/src/HOL/Nominal/nominal_induct.ML Sat May 30 19:29:21 2015 +0200 +++ b/src/HOL/Nominal/nominal_induct.ML Sat May 30 20:21:53 2015 +0200 @@ -76,7 +76,7 @@ fun rename_prems prop = let val (As, C) = Logic.strip_horn prop in Logic.list_implies (map rename As, C) end; - in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end; + in Thm.renamed_prop (rename_prems (Thm.prop_of rule)) rule end; (* nominal_induct_tac *)

--- a/src/Pure/Isar/rule_cases.ML Sat May 30 19:29:21 2015 +0200 +++ b/src/Pure/Isar/rule_cases.ML Sat May 30 20:21:53 2015 +0200 @@ -421,7 +421,7 @@ fun rename_prems prop = let val (As, C) = Logic.strip_horn prop in Logic.list_implies (map rename As, C) end; - in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end; + in Thm.renamed_prop (rename_prems (Thm.prop_of rule)) rule end;

--- a/src/Pure/drule.ML Sat May 30 19:29:21 2015 +0200 +++ b/src/Pure/drule.ML Sat May 30 20:21:53 2015 +0200 @@ -829,19 +829,16 @@ fun rename_bvars [] thm = thm | rename_bvars vs thm = let - val thy = Thm.theory_of_thm thm; - fun ren (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x |> the_default x, T, ren t) - | ren (t $ u) = ren t $ ren u - | ren t = t; - in Thm.equal_elim (Thm.reflexive (Thm.global_cterm_of thy (ren (Thm.prop_of thm)))) thm end; + fun rename (Abs (x, T, t)) = Abs (AList.lookup (op =) vs x |> the_default x, T, rename t) + | rename (t $ u) = rename t $ rename u + | rename a = a; + in Thm.renamed_prop (rename (Thm.prop_of thm)) thm end; (* renaming in left-to-right order *) fun rename_bvars' xs thm = let - val thy = Thm.theory_of_thm thm; - val prop = Thm.prop_of thm; fun rename [] t = ([], t) | rename (x' :: xs) (Abs (x, T, t)) = let val (xs', t') = rename xs t @@ -849,12 +846,12 @@ | rename xs (t $ u) = let val (xs', t') = rename xs t; - val (xs'', u') = rename xs' u + val (xs'', u') = rename xs' u; in (xs'', t' $ u') end | rename xs t = (xs, t); in - (case rename xs prop of - ([], prop') => Thm.equal_elim (Thm.reflexive (Thm.global_cterm_of thy prop')) thm + (case rename xs (Thm.prop_of thm) of + ([], prop') => Thm.renamed_prop prop' thm | _ => error "More names than abstractions in theorem") end;

--- a/src/Tools/induct.ML Sat May 30 19:29:21 2015 +0200 +++ b/src/Tools/induct.ML Sat May 30 20:21:53 2015 +0200 @@ -617,11 +617,10 @@ (case filter (fn x' => x' = x) xs of [] => xs | [_] => xs | _ => index 1 xs); in Logic.list_rename_params xs' A end; - fun rename_prop p = - let val (As, C) = Logic.strip_horn p + fun rename_prop prop = + let val (As, C) = Logic.strip_horn prop in Logic.list_implies (map rename_asm As, C) end; - val cp' = cterm_fun rename_prop (Thm.cprop_of thm); - val thm' = Thm.equal_elim (Thm.reflexive cp') thm; + val thm' = Thm.renamed_prop (rename_prop (Thm.prop_of thm)) thm; in [Rule_Cases.save thm thm'] end | special_rename_params _ _ ths = ths;