equal
deleted
inserted
replaced
83 |> Local_Theory.exit_global |
83 |> Local_Theory.exit_global |
84 |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) |
84 |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) |
85 |
85 |
86 val (qs, lthy2) = define_qconsts qtys perm_specs lthy1 |
86 val (qs, lthy2) = define_qconsts qtys perm_specs lthy1 |
87 |
87 |
88 val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws (Local_Theory.target_of lthy2) |
88 val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2 |
89 |
89 |
90 val lifted_perm_laws = |
90 val lifted_perm_laws = |
91 map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws' |
91 map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws' |
92 |> Variable.exportT lthy3 lthy2 |
92 |> Variable.exportT lthy3 lthy2 |
93 |
93 |