equal
deleted
inserted
replaced
121 in |
121 in |
122 Thm.rename_boundvars trm trm' th |
122 Thm.rename_boundvars trm trm' th |
123 end |
123 end |
124 |
124 |
125 fun lift_thm ctxt qtys simps thm = |
125 fun lift_thm ctxt qtys simps thm = |
126 thm |
126 let |
127 |> Quotient_Tacs.lifted ctxt qtys simps |
127 val ((_, [thm']), ctxt') = Variable.importT [thm] ctxt |
|
128 in |
|
129 thm' |
|
130 |> Quotient_Tacs.lifted ctxt' qtys simps |
|
131 |> singleton (ProofContext.export ctxt' ctxt) |
128 |> unraw_bounds_thm |
132 |> unraw_bounds_thm |
129 |> unraw_vars_thm |
133 |> unraw_vars_thm |
130 |> Drule.zero_var_indexes |
134 |> Drule.zero_var_indexes |
131 |
135 end |
132 |
136 |
133 end (* structure *) |
137 end (* structure *) |
134 |
138 |