167 |
167 |
168 (* initialize istate for Detail_Set *) |
168 (* initialize istate for Detail_Set *) |
169 fun init_detail (Tactic.Rewrite_Set rls) t = |
169 fun init_detail (Tactic.Rewrite_Set rls) t = |
170 let |
170 let |
171 val thy = ThyC.get_theory "Isac_Knowledge" |
171 val thy = ThyC.get_theory "Isac_Knowledge" |
172 val args = Auto_Prog.gen thy t (assoc_rls rls) |> Program.formal_args |
172 val ctxt = Proof_Context.init_global thy |
|
173 val args = Auto_Prog.gen thy t (get_rls ctxt rls) |> Program.formal_args |
173 in |
174 in |
174 Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true [(hd args, t)]) |
175 Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true [(hd args, t)]) |
175 end |
176 end |
176 | init_detail (Tactic.Rewrite_Set_Inst (subs, rls)) t = |
177 | init_detail (Tactic.Rewrite_Set_Inst (subs, rls)) t = |
177 let |
178 let |
178 val ctxt = Proof_Context.init_global (ThyC.get_theory "Isac_Knowledge") |
179 val thy = ThyC.get_theory "Isac_Knowledge" |
179 val rls' = assoc_rls rls |
180 val ctxt = Proof_Context.init_global thy |
|
181 val rls' = get_rls ctxt rls |
180 val v = case Subst.T_from_input ctxt subs of |
182 val v = case Subst.T_from_input ctxt subs of |
181 (_, v) :: _ => v (*...we suppose the substitution of only ONE bound variable*) |
183 (_, v) :: _ => v (*...we suppose the substitution of only ONE bound variable*) |
182 | _ => raise ERROR "init_detail: uncovered case" |
184 | _ => raise ERROR "init_detail: uncovered case" |
183 val prog = Auto_Prog.gen (Proof_Context.theory_of ctxt) t rls' |
185 val prog = Auto_Prog.gen thy t rls' |
184 val args = Program.formal_args prog |
186 val args = Program.formal_args prog |
185 in |
187 in |
186 Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true (args ~~ [t, v])) |
188 Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true (args ~~ [t, v])) |
187 end |
189 end |
188 | init_detail tac _ = raise ERROR ("init_detail: uncovered definition for " ^ Tactic.input_to_string tac) |
190 | init_detail tac _ = |
189 |
191 raise ERROR ("init_detail: uncovered definition for " ^ Tactic.input_to_string tac) |
190 (** initialisation **) |
|
191 |
|
192 |
|
193 |
192 |
194 (**)end(**) |
193 (**)end(**) |
195 |
194 |