equal
deleted
inserted
replaced
103 val lthy1 = |
103 val lthy1 = |
104 lthy |
104 lthy |
105 |> Local_Theory.exit_global |
105 |> Local_Theory.exit_global |
106 |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) |
106 |> Class.instantiation (qfull_ty_names, tvs, @{sort pt}) |
107 |
107 |
108 val (qs, lthy2) = define_qconsts qtys perm_specs lthy1 |
108 val (_, lthy2) = define_qconsts qtys perm_specs lthy1 |
109 |
109 |
110 val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2 |
110 val ((_, raw_perm_laws'), lthy3) = Variable.importT raw_perm_laws lthy2 |
111 |
111 |
112 val lifted_perm_laws = |
112 val lifted_perm_laws = |
113 map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws' |
113 map (Quotient_Tacs.lifted lthy3 qtys []) raw_perm_laws' |