author | Christian Urban <urbanc@in.tum.de> |
Wed, 29 Feb 2012 03:13:45 +0000 | |
changeset 3127 | d13ac9f4e773 |
parent 3126 | d3d5225f4f24 (current diff) |
parent 3124 | 528704b5830e (diff) |
child 3128 | 4bad521e3b9e |
--- a/Nominal/nominal_dt_alpha.ML Wed Feb 29 03:12:52 2012 +0000 +++ b/Nominal/nominal_dt_alpha.ML Wed Feb 29 03:13:45 2012 +0000 @@ -283,7 +283,7 @@ alpha_bn_tys = alpha_bn_tys, alpha_intros = alpha_intros, alpha_cases = alpha_cases, - alpha_raw_induct = alpha_raw_induct}, lthy') + alpha_raw_induct = alpha_raw_induct}, Local_Theory.restore lthy') end