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 let |
126 thm |
127 val ((_, [thm']), ctxt') = Variable.importT [thm] ctxt |
127 |> Quotient_Tacs.lifted ctxt qtys simps |
128 in |
|
129 thm' |
|
130 |> Quotient_Tacs.lifted ctxt' qtys simps |
|
131 |> singleton (ProofContext.export ctxt' ctxt) |
|
132 |> unraw_bounds_thm |
128 |> unraw_bounds_thm |
133 |> unraw_vars_thm |
129 |> unraw_vars_thm |
134 |> Drule.zero_var_indexes |
130 |> Drule.zero_var_indexes |
135 end |
|
136 |
131 |
137 end (* structure *) |
132 end (* structure *) |
138 |
133 |